diff options
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 53 |
1 files changed, 44 insertions, 9 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 82a2de094..be6250257 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -8,6 +8,14 @@ open Names +(** {6 Value under universe substitution } *) +type 'a puniverses = 'a Univ.puniverses + +(** {6 Simply type aliases } *) +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses + (** {6 Existential variables } *) type existential_key = Evar.t @@ -88,20 +96,26 @@ val mkLetIn : Name.t * constr * types * constr -> constr {% $(f~t_1~\dots~t_n)$ %}. *) val mkApp : constr * constr array -> constr -(** Constructs a constant - The array of terms correspond to the variables introduced in the section *) +val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses + +(** Constructs a constant *) val mkConst : constant -> constr +val mkConstU : pconstant -> constr + +(** Constructs a projection application *) +val mkProj : (constant * constr) -> constr (** Inductive types *) -(** Constructs the ith (co)inductive type of the block named kn - The array of terms correspond to the variables introduced in the section *) +(** Constructs the ith (co)inductive type of the block named kn *) val mkInd : inductive -> constr +val mkIndU : pinductive -> constr (** Constructs the jth constructor of the ith (co)inductive type of the - block named kn. The array of terms correspond to the variables - introduced in the section *) + block named kn. *) val mkConstruct : constructor -> constr +val mkConstructU : pconstructor -> constr +val mkConstructUi : pinductive * int -> constr (** Constructs a destructor of inductive type. @@ -170,12 +184,13 @@ type ('constr, 'types) kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of constant - | Ind of inductive - | Construct of constructor + | Const of constant puniverses + | Ind of inductive puniverses + | Construct of constructor puniverses | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint + | Proj of constant * 'constr (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative @@ -187,6 +202,26 @@ val kind : constr -> (constr, types) kind_of_term and application grouping *) val equal : constr -> constr -> bool +(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [c]. *) +val eq_constr_univs : constr Univ.check_function + +(** [leq_constr_univs a b] [true, c] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [c]. *) +val leq_constr_univs : constr Univ.check_function + +(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [c]. *) +val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained + +(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [c]. *) +val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained + +(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and ignoring universe instances. *) +val eq_constr_nounivs : constr -> constr -> bool + (** Total ordering compatible with [equal] *) val compare : constr -> constr -> int |