GammaR.rkt (404B)
1 #lang at-exp s-exp phc-thesis/scribblings/equations-lang 2 3 @; This file is NOT under the CC0 license, as it contains rules and definitions 4 @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the 5 @; permission to copy these rules, but did not ask for a relicensing under the 6 @; CC0 license. 7 8 #:Γ 9 10 @$${ 11 @Γ[⊢ e R] 12 } 13 14 #:R 15 16 @cases[@R #:first-sep "⩴" 17 @R[τ φ⁺ φ⁻ o]]