diff options
| author | courant | 2003-06-27 13:35:03 +0000 |
|---|---|---|
| committer | courant | 2003-06-27 13:35:03 +0000 |
| commit | afe6690652949d92bfbcf34194836364884b7111 (patch) | |
| tree | 5a5dc1f4c8c681f6cb2156dd6083a4671364e700 /kernel/term.mli | |
| parent | 293b31aab50f0b7f947960ce15bf9ae6b6d576de (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4209 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 1e7a6e08e0..472ffb2c87 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -80,7 +80,7 @@ val body_of_type : types -> constr (*s Term constructors. *) -(* Constructs a DeBrujin index *) +(* Constructs a DeBrujin index (DB indices begin at 1) *) val mkRel : int -> constr (* Constructs a Variable *) @@ -325,7 +325,6 @@ val mkNamedProd_wo_LetIn : named_declaration -> types -> types val mkLambda_or_LetIn : rel_declaration -> constr -> constr val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr - (*s Other term constructors. *) val abs_implicit : constr -> constr @@ -343,14 +342,28 @@ val appvectc : constr -> constr array -> constr where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *) val prodn : int -> (name * constr) list -> constr -> constr +(* [compose_prod l b] = $(x_1:T_1)..(x_n:T_n)b$ + where $l = [(x_n,T_n);\dots;(x_1,T_1)]$. + Inverse of [decompose_prod]. *) +val compose_prod : (name * constr) list -> constr -> constr + (* [lamn n l b] = $[x_1:T_1]..[x_n:T_n]b$ where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *) val lamn : int -> (name * constr) list -> constr -> constr +(* [compose_lam l b] = $[x_1:T_1]..[x_n:T_n]b$ + where $l = [(x_n,T_n);\dots;(x_1,T_1)]$. + Inverse of [decompose_lam] *) +val compose_lam : (name * constr) list -> constr -> constr + (* [to_lambda n l] - = $[x_1:T_1]...[x_n:T_n](x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$ - where $l = (x_1:T_1)...(x_n:T_n)(x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$ *) + = $[x_1:T_1]...[x_n:T_n]T$ + where $l = (x_1:T_1)...(x_n:T_n)T$ *) val to_lambda : int -> constr -> constr + +(* [to_prod n l] + = $(x_1:T_1)...(x_n:T_n)T$ + where $l = [x_1:T_1]...[x_n:T_n]T$ *) val to_prod : int -> constr -> constr (* pseudo-reduction rule *) @@ -415,6 +428,9 @@ val noccur_with_meta : int -> int -> constr -> bool (*s Relocation and substitution *) +(* [exliftn el c] lifts [c] with lifting [el] *) +val exliftn : Esubst.lift -> constr -> constr + (* [liftn n k c] lifts by [n] indexes above [k] in [c] *) val liftn : int -> int -> constr -> constr |