diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 51406b1e08..7320b8be89 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -164,6 +164,9 @@ val mkCast : constr -> constr -> constr (* Constructs the product $(x:t_1)t_2$. $x$ may be anonymous. *) val mkProd : name -> constr -> constr -> constr +(* [mkProd_string s t c] constructs the product $(s:t)c$ *) +val mkProd_string : string -> constr -> constr -> constr + (* non-dependant product $t_1 \rightarrow t_2$ *) val mkArrow : constr -> constr -> constr @@ -174,6 +177,9 @@ val mkNamedProd : identifier -> constr -> constr -> constr val mkLambda : name -> constr -> constr -> constr val mkNamedLambda : identifier -> constr -> constr -> constr +(* [mkLambda_string s t c] constructs $[s:t]c$ *) +val mkLambda_string : string -> constr -> constr -> constr + (* If $a = [| t_1; \dots; t_n |]$, constructs the application $(t_1~\dots~t_n)$. *) val mkAppL : constr array -> constr |