diff options
| author |  Jasper Hugunin <jasper@hashplex.com> | 2017-12-19 14:08:58 +0900 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2017-12-19 14:08:58 +0900 |
| commit | cf81bf01602ef5ab725b604f5c243a83adf8d31c (patch) | |
| tree | 8234aae34628168c95d9018621654ac6886083cb /kernel/constr.mli | |
| parent | 80158e796b6df8eb36117f349c312127c5729a8c (diff) | |
Fix order of let-in representation comment.
The comment had the type and value of the let-in swapped, which contradicted the listed types.
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 21c477578..98bf71308 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -203,7 +203,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) - | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *) + | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:C := B in D"] is represented as [LetIn (A,B,C,D)]. *) | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])]. The {!mkApp} constructor also enforces the following invariant: |