diff options
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 41 |
1 files changed, 28 insertions, 13 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index f897448557..25ceffbd04 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -77,6 +77,9 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t For getting the evar-normal form of a term with evars see {!Evarutil.nf_evar}. *) +val to_constr_opt : Evd.evar_map -> t -> Constr.t option +(** Same as [to_constr], but returns [None] if some unresolved evars remain *) + val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type (** {5 Constructors} *) @@ -101,13 +104,14 @@ val mkVar : Id.t -> t val mkMeta : metavariable -> t val mkEvar : t pexistential -> t val mkSort : Sorts.t -> t +val mkSProp : t val mkProp : t val mkSet : t val mkType : Univ.Universe.t -> t val mkCast : t * cast_kind * t -> t -val mkProd : Name.t * t * t -> t -val mkLambda : Name.t * t * t -> t -val mkLetIn : Name.t * t * t * t -> t +val mkProd : Name.t Context.binder_annot * t * t -> t +val mkLambda : Name.t Context.binder_annot * t * t -> t +val mkLetIn : Name.t Context.binder_annot * t * t * t -> t val mkApp : t * t array -> t val mkConst : Constant.t -> t val mkConstU : Constant.t * EInstance.t -> t @@ -120,18 +124,25 @@ val mkConstructUi : (inductive * EInstance.t) * int -> t val mkCase : case_info * t * t * t array -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t -val mkArrow : t -> t -> t +val mkArrow : t -> Sorts.relevance -> t -> t +val mkArrowR : t -> t -> t +val mkInt : Uint63.t -> t + +val mkRef : GlobRef.t * EInstance.t -> t + +val type1 : t val applist : t * t list -> t +val applistc : t -> t list -> t val mkProd_or_LetIn : rel_declaration -> t -> t val mkLambda_or_LetIn : rel_declaration -> t -> t val it_mkProd_or_LetIn : t -> rel_context -> t val it_mkLambda_or_LetIn : t -> rel_context -> t -val mkNamedLambda : Id.t -> types -> constr -> constr -val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr -val mkNamedProd : Id.t -> types -> types -> types +val mkNamedLambda : Id.t Context.binder_annot -> types -> constr -> constr +val mkNamedLetIn : Id.t Context.binder_annot -> constr -> types -> constr -> constr +val mkNamedProd : Id.t Context.binder_annot -> types -> types -> types val mkNamedLambda_or_LetIn : named_declaration -> types -> types val mkNamedProd_or_LetIn : named_declaration -> types -> types @@ -155,6 +166,8 @@ val isCoFix : Evd.evar_map -> t -> bool val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool +val isType : Evd.evar_map -> constr -> bool + type arity = rel_context * ESorts.t val destArity : Evd.evar_map -> types -> arity val isArity : Evd.evar_map -> t -> bool @@ -167,9 +180,9 @@ val destMeta : Evd.evar_map -> t -> metavariable val destVar : Evd.evar_map -> t -> Id.t val destSort : Evd.evar_map -> t -> ESorts.t val destCast : Evd.evar_map -> t -> t * cast_kind * t -val destProd : Evd.evar_map -> t -> Name.t * types * types -val destLambda : Evd.evar_map -> t -> Name.t * types * t -val destLetIn : Evd.evar_map -> t -> Name.t * t * types * t +val destProd : Evd.evar_map -> t -> Name.t Context.binder_annot * types * types +val destLambda : Evd.evar_map -> t -> Name.t Context.binder_annot * types * t +val destLetIn : Evd.evar_map -> t -> Name.t Context.binder_annot * t * types * t val destApp : Evd.evar_map -> t -> t * t array val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t val destEvar : Evd.evar_map -> t -> t pexistential @@ -180,10 +193,12 @@ val destProj : Evd.evar_map -> t -> Projection.t * t val destFix : Evd.evar_map -> t -> (t, t) pfixpoint val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint +val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t + val decompose_app : Evd.evar_map -> t -> t * t list (** Pops lambda abstractions until there are no more, skipping casts. *) -val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t +val decompose_lam : Evd.evar_map -> t -> (Name.t Context.binder_annot * t) list * t (** Pops lambda abstractions and letins until there are no more, skipping casts. *) val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t @@ -199,10 +214,10 @@ val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t @raise UserError if the term doesn't have enough lambdas/letins. *) val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t -val compose_lam : (Name.t * t) list -> t -> t +val compose_lam : (Name.t Context.binder_annot * t) list -> t -> t val to_lambda : Evd.evar_map -> int -> t -> t -val decompose_prod : Evd.evar_map -> t -> (Name.t * t) list * t +val decompose_prod : Evd.evar_map -> t -> (Name.t Context.binder_annot * t) list * t val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t |