diff options
| author | Matej Kosik | 2015-12-16 12:33:58 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-18 15:57:38 +0100 |
| commit | 98065338c54717fd2d7aa887e8693acdc1cff5ba (patch) | |
| tree | f7b853e054912cc582c36b50f3348950649e2bd0 /kernel | |
| parent | e181c9b043e64342c1e51763f4fe88c78bc4736d (diff) | |
COMMENTS: added to some variants of the "Constr.kind_of_term" type.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.mli | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 5a370d31d8..70f1699314 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -93,8 +93,9 @@ val mkLambda : Name.t * types * constr -> constr (** Constructs the product [let x = t1 : t2 in t3] *) val mkLetIn : Name.t * constr * types * constr -> constr -(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application - {% $(f~t_1~\dots~t_n)$ %}. *) +(** [mkApp (f, [|t1; ...; tN|]] constructs the application + {%html:(f t<sub>1</sub> ... t<sub>n</sub>)%} + {%latex:$(f~t_1\dots f_n)$%}. *) val mkApp : constr * constr array -> constr val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses @@ -181,10 +182,13 @@ type ('constr, 'types) kind_of_term = | Evar of 'constr pexistential | Sort of Sorts.t | Cast of 'constr * cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array + | 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)]. *) + | 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: + - [F] itself is not {!App} + - and [[|P1;..;Pn|]] is not empty. *) | Const of constant puniverses | Ind of inductive puniverses | Construct of constructor puniverses |