adt-Ectx.scrbl.old (939B)
1 #lang scribble/manual 2 3 @require["util.rkt" 4 "adt-utils.rkt" 5 (for-label (only-meta-in 0 typed/racket))] 6 @(use-mathjax) 7 8 @title[#:style (with-html5 manual-doc-style) 9 #:version (version-text)]{Evaluation contexts} 10 11 @$${ 12 @cases["E" #:first-sep "⩴" 13 @acase{…} 14 @acase{@ctor[@κ E]@tag*{constructor instance}} 15 @acase{(@ctor-pred[@κ] E)@tag*{constructor predicate}} 16 @acase{(@ctor-val[@κ] E)@tag*{constructor value access}} 17 @acase{@record[@repeated{@|ɐ|ᵢ = vᵢ} 18 @${@|ɐ|ⱼ = E} 19 @repeated{@|ɐ|ₖ = eₖ}]@tag*{record instance}} 20 @acase{(@record-pred[@repeated{@|ɐ|ᵢ}] E)@tag*{record predicate}} 21 @acase{E.@|ɐ|@tag*{record field access}} 22 @acase{@opwith[E @|ɐ| e]@tag*{record update (new/change)}} 23 @acase{@opwith[v @|ɐ| E]} 24 @acase{@opwithout[E @|ɐ|]@tag*{record update (remove)}}] 25 }