Add documentation comments.

This commit is contained in:
François Pottier 2022-04-08 10:48:14 +02:00
parent 21fe5539aa
commit a1dc9edf20
1 changed files with 6 additions and 0 deletions

View File

@ -246,6 +246,9 @@ module Make
type variable [α] to a constraint, as in {!exist}.) On paper, we write
[let x = λα.c1(α) in c2] for this constraint.
This constraint requires [α.c1(α)] to be satisfied. This is required
even if the term variable [x] is not used in [c2].
Inside [c2], an instantiation constraint of the form [x(β)] is logically
equivalent to [c1(β)]. In other words, a [let] constraint acts like a
macro definition: every use of the variable [x] in the scope of this
@ -294,6 +297,9 @@ module Make
Every other type variable in the list [αs] is considered
existentially bound in this constraint abstraction.
This constraint requires [αs.c1(αs)] to be satisfied. This is required
even if some of the term variables in the list [xs] are not used in [c2].
The semantic value of this constraint is a tuple of:
- a list [γs] of decoded type variables that may appear in the semantic
value [v1] (see {!let1}).