v.rkt (1257B)
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 @cases["v" #:first-sep "⩴" 9 @acase{@primop @tag*{primitive function}} 10 @acase{@num-v @tag*{number}} 11 @acase{@true-v @tag*{booleans}} 12 @acase{@false-v} 13 @acase{@λv[(@repeated{x:τ}) e] @tag*{lambda function}} 14 @acase{@λv[(@repeated{x:τ} @${\ .\ } @${x:τ*}) e] 15 @tag*{variadic function}} 16 @acase{@λv[(@repeated{x:τ} @${\ .\ } @${x:@polydot[τ α]}) e] 17 @tag*{variadic polymorphic function}} 18 @acase{@Λv[(@repeated{α}) e] 19 @tag*{polymorphic abstraction}} 20 @acase{@Λv[(@repeated{α} @polydotα[α]) e] 21 @tag*{variadic polymorphic abstraction}} 22 @acase{@consv[v v] @tag*{pair}} 23 @acase{@null-v @tag*{null}} 24 @acase{@promisev[e] @tag*{promise}} 25 @acase{@symv[@sym*] @tag*{symbol}}] 26 27 #:listv 28 29 @$${ 30 \begin{aligned} 31 @listv[v₀ @repeated{vᵢ}] &≝ @consv[v₀ @listv[@repeated{vᵢ}]] \\ 32 @listv[] &≝ @null-v \\ 33 \end{aligned} 34 }