adt-row-Ectx.scrbl (1086B)
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 (with ρ)} 10 11 @$${ 12 @cases["E" #:first-sep "⩴" 13 @acase{…} 14 @acase{@ctore[@κ E]@tag*{constructor instance}} 15 @acase{(@ctor-pred[@κ]\ E)@tag*{constructor predicate}} 16 @acase{(@ctor-val[@κ]\ E)@tag*{constructor value access}} 17 @acase{@recorde[@repeated{@|ɐ|ᵢ = vᵢ} 18 @${@|ɐ|ⱼ = E} 19 @repeated{@|ɐ|ₖ = eₖ}]@tag*{record instance}} 20 @acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ E)@tag*{record predicate}} 21 @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ E) 22 @tag*{row-polymorphic record predicate}} 23 @acase{E.@|ɐ|@tag*{record field access}} 24 @acase{@opwith[E @|ɐ| e]@tag*{record update (new/change)}} 25 @acase{@opwith[v @|ɐ| E]} 26 @acase{@opwithout[E @|ɐ|]@tag*{record update (remove)}}] 27 }