diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 35 |
1 files changed, 12 insertions, 23 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index d36a3a36f3..d5aaf6ad06 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -68,20 +68,21 @@ type ('constr, 'types) prec_declaration = type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = +type ('constr, 'types, 'sort, 'univs) kind_of_term = + ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = | Rel of int | Var of Id.t | Meta of metavariable | Evar of 'constr pexistential - | Sort of sorts + | Sort of 'sort | 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 - | Const of constant puniverses - | Ind of inductive puniverses - | Construct of constructor puniverses + | Const of (constant * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint @@ -98,7 +99,6 @@ val isVarId : Id.t -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool -val isMetaOf : metavariable -> constr -> bool val isEvar_or_Meta : constr -> bool val isSort : constr -> bool val isCast : constr -> bool @@ -127,7 +127,7 @@ val is_small : sorts -> bool exception DestKO -(** Destructs a DeBrujin index *) +(** Destructs a de Bruijn index *) val destRel : constr -> int (** Destructs an existential variable *) @@ -349,20 +349,6 @@ val strip_lam_n : int -> constr -> constr val strip_prod_assum : types -> types val strip_lam_assum : constr -> constr -(** Flattens application lists *) -val collapse_appl : constr -> constr - - -(** Remove recursively the casts around a term i.e. - [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : constr -> constr - -(** Apply a function letting Casted types in place *) -val under_casts : (constr -> constr) -> constr -> constr - -(** Apply a function under components of Cast if any *) -val under_outer_cast : (constr -> constr) -> constr -> constr - (** {5 ... } *) (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types @@ -458,12 +444,15 @@ val leq_constr_univs : constr UGraph.check_function application grouping and ignoring universe instances. *) val eq_constr_nounivs : constr -> constr -> bool -val kind_of_term : constr -> (constr, types) kind_of_term +val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term (** Alias for [Constr.kind] *) -val constr_ord : constr -> constr -> int +val compare : constr -> constr -> int (** Alias for [Constr.compare] *) +val constr_ord : constr -> constr -> int +(** Alias for [Term.compare] *) + val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a (** Alias for [Constr.fold] *) |