adt-pe.scrbl.old (1162B)
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)]{Path elements} 10 11 @$${pe ⩴ … @P @πctor-val @P @|ɐ|} 12 13 We extend the metafunctions for paths given 14 in@~cite[#:precision "pp. 65 and 75" "tobin-hochstadt_typed_2010"]. The @${ 15 @update} metafunction is used when using filters to restrict the type 16 of a (subpart of a) local variable in the @tt{then} and @tt{else} branches of 17 a conditional. 18 19 @todo{∷ is not defined in@~cite["tobin-hochstadt_typed_2010"], we have to 20 define it.} 21 22 @todo{How should I note cleanly these removals / replacements which refer to 23 an @|ɐ| and its τ or @${v} inside the set of @${@|ɐ|ᵢ}?} 24 25 @$${ 26 @aligned{ 27 @update(@record[@repeated{@|ɐ|ᵢ : τᵢ}ⁿ], υ_{π∷@|ɐ|ⱼ}) 28 &= @record[@${@repeated{@|ɐ|ᵢ : τᵢ} ∖ \{@|ɐ|ⱼ : τⱼ\}} 29 @${@|ɐ|ⱼ : @${@update(τⱼ, υ_π)}}] 30 \\ 31 &\quad @where @|ɐ|ⱼ : τⱼ ∈ @repeatset{@|ɐ|ᵢ : τᵢ}\\ 32 @update(@ctor[@κ τ], υ_{π∷@πctor-val}) 33 &= @ctor[@κ @${@update(τ, υ_π)}] 34 } 35 }