commit bc9e7d18a4eb2018463764af6db809ed72c6a502
parent 481e4f8fd00149714d462142086f463a45f25a43
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Wed, 16 Aug 2017 17:13:14 +0200
Cleanup, moved subsection.
Diffstat:
3 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/scribblings/adt-row-Ectx.scrbl b/scribblings/adt-row-Ectx.scrbl
@@ -18,7 +18,8 @@
@${@|ɐ|ⱼ = E}
@repeated{@|ɐ|ₖ = eₖ}]@tag*{record instance}}
@acase{(@record-pred[@repeatset{@|ɐ|ᵢ}]\ E)@tag*{record predicate}}
- @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ E)@tag*{row-polymorphic record predicate}}
+ @acase{(@record-pred*[@repeatset{@|ɐ|ᵢ} @repeatset{-@|ɐ|ⱼ}]\ E)
+ @tag*{row-polymorphic record predicate}}
@acase{E.@|ɐ|@tag*{record field access}}
@acase{@opwith[E @|ɐ| e]@tag*{record update (new/change)}}
@acase{@opwith[v @|ɐ| E]}
diff --git a/scribblings/adt-row-e.scrbl b/scribblings/adt-row-e.scrbl
@@ -53,10 +53,14 @@ the value stored in an instance of a constructor.
instantiation operators are @atc[e @repeated{@ςc}] and @atf[e @repeated{@ςf}].
}
@acase{…}
- @acase{@Λce[(@repeated{@ρc}) e]@tag*{row-polymorphic abstraction (constructors)}}@; new
- @acase{@Λfe[(@repeated{@ρf}) e]@tag*{row-polymorphic abstraction (fields)}}@; new
- @acase{@atc[e @repeated{@ςc}]@tag*{row-polymorphic instantiation (constructors)}}@; new
- @acase{@atf[e @repeated{@ςf}]@tag*{row-polymorphic instantiation (fields)}}]@; new
+ @acase{@Λce[(@repeated{@ρc}) e]
+ @tag*{row-polymorphic abstraction (constructors)}}@; new
+ @acase{@Λfe[(@repeated{@ρf}) e]
+ @tag*{row-polymorphic abstraction (fields)}}@; new
+ @acase{@atc[e @repeated{@ςc}]
+ @tag*{row-polymorphic instantiation (constructors)}}@; new
+ @acase{@atf[e @repeated{@ςf}]
+ @tag*{row-polymorphic instantiation (fields)}}]@; new
@;{
Note: In the @${@record[@repeated{@|ɐ|ᵢ = eᵢ}]} expression, which builds a
diff --git a/scribblings/adt.scrbl b/scribblings/adt.scrbl
@@ -24,10 +24,10 @@ constants, i.e. they are written literally in the program source.
@$${@κ ⩴ name ∈ 𝒞}
@$${@ɐ ⩴ name ∈ ℱ}
+@include-asection["adt-row-tausigma.scrbl"]
@include-asection["adt-row-e.scrbl"]
@include-asection["adt-row-v.scrbl"]
@include-asection["adt-row-Ectx.scrbl"]
-@include-asection["adt-row-tausigma.scrbl"]
@include-asection["adt-row-te.scrbl"]
@include-asection["adt-row-sub.scrbl"]
@include-asection["adt-row-pe.scrbl"]