package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = Evd.econstr

Type of incomplete terms. Essentially a wrapper around Constr.t ensuring that Constr.kind does not observe defined evars.

Universe variables
module ERelevance : sig ... end
module ESorts : sig ... end
module EInstance : sig ... end
type types = t
type constr = t
type existential = t Constr.pexistential
type case_return = (t, ERelevance.t) Constr.pcase_return
type case_branch = (t, ERelevance.t) Constr.pcase_branch
type rec_declaration = (t, t, ERelevance.t) Constr.prec_declaration
type fixpoint = (t, t, ERelevance.t) Constr.pfixpoint
type cofixpoint = (t, t, ERelevance.t) Constr.pcofixpoint
type unsafe_judgment = (constr, types) Environ.punsafe_judgment
type unsafe_type_judgment = (types, Evd.esorts) Environ.punsafe_type_judgment
type named_context = (constr, types, ERelevance.t) Context.Named.pt
type compacted_context = compacted_declaration list
type rel_context = (constr, types, ERelevance.t) Context.Rel.pt
type 'a binder_annot = ('a, ERelevance.t) Context.pbinder_annot
val annotR : 'a -> 'a binder_annot
type case_invert = t Constr.pcase_invert
type 'a puniverses = 'a * EInstance.t
Destructors

Same as Constr.kind except that it expands evars and normalizes universes on the fly.

val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t

Returns the evar-normal form of the argument. Note that this function is supposed to be called when the original term has not more free-evars anymore. If you need compatibility with the old semantics, set abort_on_undefined_evars to false.

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

type kind_of_type =
  1. | SortType of ESorts.t
  2. | CastType of types * t
  3. | ProdType of Names.Name.t binder_annot * t * t
  4. | LetInType of Names.Name.t binder_annot * t * t * t
  5. | AtomicType of t * t array
val kind_of_type : Evd.evar_map -> t -> kind_of_type
Constructors

Construct a term from a view.

val of_constr : Constr.t -> t

Translate a kernel term into an incomplete term in O(1).

Insensitive primitives

Evar-insensitive versions of the corresponding functions. See the Constr module for more information.

Constructors
val mkRel : int -> t
val mkVar : Names.Id.t -> t
val mkMeta : Constr.metavariable -> t
val mkEvar : t Constr.pexistential -> t
val mkSort : ESorts.t -> t
val mkSProp : t
val mkProp : t
val mkSet : t
val mkType : Univ.Universe.t -> t
val mkCast : (t * Constr.cast_kind * t) -> t
val mkProd : (Names.Name.t binder_annot * t * t) -> t
val mkLambda : (Names.Name.t binder_annot * t * t) -> t
val mkLetIn : (Names.Name.t binder_annot * t * t * t) -> t
val mkApp : (t * t array) -> t
val mkConstU : (Names.Constant.t * EInstance.t) -> t
val mkProj : (Names.Projection.t * ERelevance.t * t) -> t
val mkIndU : (Names.inductive * EInstance.t) -> t
val mkConstructU : (Names.constructor * EInstance.t) -> t
val mkConstructUi : ((Names.inductive * EInstance.t) * int) -> t
val mkCase : case -> t
val mkFix : (t, t, ERelevance.t) Constr.pfixpoint -> t
val mkCoFix : (t, t, ERelevance.t) Constr.pcofixpoint -> t
val mkArrow : t -> ERelevance.t -> t -> t
val mkArrowR : t -> t -> t
val mkInt : Uint63.t -> t
val mkFloat : Float64.t -> t
val mkString : Pstring.t -> t
val mkArray : (EInstance.t * t array * t * t) -> t
module UnsafeMonomorphic : sig ... end
val mkConst : Names.Constant.t -> t
  • deprecated Use [mkConstU] or if truly needed [UnsafeMonomorphic.mkConst]
val mkInd : Names.inductive -> t
  • deprecated Use [mkIndU] or if truly needed [UnsafeMonomorphic.mkInd]
val mkConstruct : Names.constructor -> t
  • deprecated Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct]
val mkRef : (Names.GlobRef.t * EInstance.t) -> t
val type1 : t
val applist : (t * t list) -> t
val applistc : t -> t list -> t

Abstracting/generalizing over binders

it = iterated or_LetIn = turn a local definition into a LetIn wo_LetIn = inlines local definitions (i.e. substitute them in the body) Named = binding is by name and the combinators turn it into a binding by index (complexity is nb(binders) * size(term))

val it_mkProd : t -> (Names.Name.t binder_annot * t) list -> t
val it_mkLambda : t -> (Names.Name.t binder_annot * 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 mkProd_wo_LetIn : rel_declaration -> t -> t
val mkLambda_wo_LetIn : rel_declaration -> t -> t
val it_mkProd_wo_LetIn : t -> rel_context -> t
val it_mkLambda_wo_LetIn : t -> rel_context -> t
val mkNamedProd : Evd.evar_map -> Names.Id.t binder_annot -> types -> types -> types
val mkNamedLambda : Evd.evar_map -> Names.Id.t binder_annot -> types -> constr -> constr
val mkNamedLetIn : Evd.evar_map -> Names.Id.t binder_annot -> constr -> types -> constr -> constr
val mkNamedProd_or_LetIn : Evd.evar_map -> named_declaration -> types -> types
val mkNamedLambda_or_LetIn : Evd.evar_map -> named_declaration -> types -> types
val it_mkNamedProd_or_LetIn : Evd.evar_map -> t -> named_context -> t
val it_mkNamedLambda_or_LetIn : Evd.evar_map -> t -> named_context -> t
val mkNamedProd_wo_LetIn : Evd.evar_map -> named_declaration -> t -> t
val it_mkNamedProd_wo_LetIn : Evd.evar_map -> t -> named_context -> t
val mkLEvar : Evd.evar_map -> (Evar.t * t list) -> t

Variant of mkEvar that removes identity variable instances from its argument.

Simple case analysis
val isRel : Evd.evar_map -> t -> bool
val isVar : Evd.evar_map -> t -> bool
val isInd : Evd.evar_map -> t -> bool
val isRef : Evd.evar_map -> t -> bool
val isEvar : Evd.evar_map -> t -> bool
val isMeta : Evd.evar_map -> t -> bool
val isSort : Evd.evar_map -> t -> bool
val isCast : Evd.evar_map -> t -> bool
val isApp : Evd.evar_map -> t -> bool
val isLambda : Evd.evar_map -> t -> bool
val isLetIn : Evd.evar_map -> t -> bool
val isProd : Evd.evar_map -> t -> bool
val isConst : Evd.evar_map -> t -> bool
val isConstruct : Evd.evar_map -> t -> bool
val isFix : Evd.evar_map -> t -> bool
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 mkArity : arity -> types
val destArity : Evd.evar_map -> types -> arity
val isArity : Evd.evar_map -> t -> bool
val isVarId : Evd.evar_map -> Names.Id.t -> t -> bool
val isRelN : Evd.evar_map -> int -> t -> bool
val isRefX : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t -> bool
val is_lib_ref : Environ.env -> Evd.evar_map -> string -> t -> bool

The string is interpreted by Coqlib.lib_ref. If it is not registered, return false.

val destRel : Evd.evar_map -> t -> int
val destMeta : Evd.evar_map -> t -> Constr.metavariable
val destVar : Evd.evar_map -> t -> Names.Id.t
val destSort : Evd.evar_map -> t -> ESorts.t
val destCast : Evd.evar_map -> t -> t * Constr.cast_kind * t
val destLambda : Evd.evar_map -> t -> Names.Name.t binder_annot * types * t
val destLetIn : Evd.evar_map -> t -> Names.Name.t binder_annot * t * types * t
val destApp : Evd.evar_map -> t -> t * t array
val destConst : Evd.evar_map -> t -> Names.Constant.t * EInstance.t
val destEvar : Evd.evar_map -> t -> t Constr.pexistential
val destConstruct : Evd.evar_map -> t -> Names.constructor * EInstance.t
val destCase : Evd.evar_map -> t -> case
val destFix : Evd.evar_map -> t -> (t, t, ERelevance.t) Constr.pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t, ERelevance.t) Constr.pcofixpoint
val decompose_app : Evd.evar_map -> t -> t * t array
val decompose_app_list : Evd.evar_map -> t -> t * t list
val decompose_lambda : Evd.evar_map -> t -> (Names.Name.t binder_annot * t) list * t

Pops lambda abstractions until there are no more, skipping casts.

val decompose_lambda_decls : Evd.evar_map -> t -> rel_context * t

Pops lambda abstractions and letins until there are no more, skipping casts.

val decompose_lambda_n : Evd.evar_map -> int -> t -> (Names.Name.t binder_annot * t) list * t

Pops n lambda abstractions, skipping casts.

  • raises UserError

    if the term doesn't have enough lambdas.

val decompose_lambda_n_assum : Evd.evar_map -> int -> t -> rel_context * t

Pops n lambda abstractions, and pop letins only if needed to expose enough lambdas, skipping casts.

  • raises UserError

    if the term doesn't have enough lambdas.

val decompose_lambda_n_decls : Evd.evar_map -> int -> t -> rel_context * t

Pops n lambda abstractions and letins, skipping casts.

  • raises UserError

    if the term doesn't have enough lambdas/letins.

val prod_decls : Evd.evar_map -> t -> rel_context
val compose_lam : (Names.Name.t binder_annot * t) list -> t -> t
  • deprecated Use [it_mkLambda] instead.
val to_lambda : Evd.evar_map -> int -> t -> t
val decompose_prod : Evd.evar_map -> t -> (Names.Name.t binder_annot * t) list * t
val decompose_prod_n : Evd.evar_map -> int -> t -> (Names.Name.t binder_annot * t) list * t
val decompose_prod_decls : Evd.evar_map -> t -> rel_context * t
val decompose_prod_n_decls : Evd.evar_map -> int -> t -> rel_context * t
val existential_type : Evd.evar_map -> existential -> types
val whd_evar : Evd.evar_map -> constr -> constr
Equality
val eq_constr : Evd.evar_map -> t -> t -> bool
val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
val eq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
val leq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
val eq_existential : Evd.evar_map -> (t -> t -> bool) -> existential -> existential -> bool
val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option

eq_constr_universes_proj can equate projections and their eta-expanded constant form.

val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
Iterators
val map : Evd.evar_map -> (t -> t) -> t -> t
val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
val map_branches : (t -> t) -> case_branch array -> case_branch array
val map_return_predicate : (t -> t) -> case_return -> case_return
val map_existential : Evd.evar_map -> (t -> t) -> existential -> existential
val iter : Evd.evar_map -> (t -> unit) -> t -> unit
val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
val iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
val fold_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> t -> 'b) -> 'a -> 'b -> t -> 'b
val universes_of_constr : Evd.evar_map -> t -> Sorts.QVar.Set.t * Univ.Level.Set.t

Gather the universes transitively used in the term, including in the type of evars appearing in it.

Substitutions
module Vars : sig ... end

See vars.mli for the documentation of the functions below

Environment handling
val push_rel_context : rel_context -> Environ.env -> Environ.env
val push_rec_types : rec_declaration -> Environ.env -> Environ.env
val push_named_context : named_context -> Environ.env -> Environ.env
val rel_context : Environ.env -> rel_context
val named_context : Environ.env -> named_context
val val_of_named_context : named_context -> Environ.named_context_val
val named_context_of_val : Environ.named_context_val -> named_context
val lookup_rel : int -> Environ.env -> rel_declaration
val map_rel_context_in_env : (Environ.env -> constr -> constr) -> Environ.env -> rel_context -> rel_context
val match_named_context_val : Environ.named_context_val -> (named_declaration * Environ.named_context_val) option
val identity_subst_val : Environ.named_context_val -> t SList.t
val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:UVars.Instance.t -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Evd.evar_map * t
val is_global : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t -> bool
  • deprecated Use [EConstr.isRefX] instead.
val annotate_case : Environ.env -> Evd.evar_map -> case -> Constr.case_info * EInstance.t * t array * ((rel_context * t) * ERelevance.t) * case_invert * t * (rel_context * t) array

Same as above, but doesn't turn contexts into binders

val expand_branch : Environ.env -> Evd.evar_map -> EInstance.t -> t array -> Names.constructor -> case_branch -> rel_context

Given a universe instance and parameters for the inductive type, constructs the typed context in which the branch lives.

Extra
val of_existential : Constr.existential -> existential
val of_named_context : Constr.named_context -> named_context
val of_rel_context : Constr.rel_context -> rel_context
val to_named_context : Evd.evar_map -> named_context -> Constr.named_context
val to_rel_context : Evd.evar_map -> rel_context -> Constr.rel_context
val of_case_invert : Constr.case_invert -> case_invert
val of_constr_array : Constr.t array -> t array
val of_binder_annot : 'a Constr.binder_annot -> 'a binder_annot
val to_binder_annot : Evd.evar_map -> 'a binder_annot -> 'a Constr.binder_annot
Unsafe operations
module Unsafe : sig ... end

Deprecated

val decompose_lambda_assum : Evd.evar_map -> t -> rel_context * t
  • deprecated Use [decompose_lambda_decls] instead.
val decompose_prod_assum : Evd.evar_map -> t -> rel_context * t
  • deprecated Use [decompose_prod_decls] instead.
val decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t
  • deprecated Use [decompose_prod_n_decls] instead.
val prod_assum : Evd.evar_map -> t -> rel_context
  • deprecated Use [prod_decls] instead.
val decompose_lam : Evd.evar_map -> t -> (Names.Name.t binder_annot * t) list * t
  • deprecated Use [decompose_lambda] instead.
val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t
  • deprecated Use [decompose_lambda_n_assum] instead.
val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t
  • deprecated Use [decompose_lambda_n_decls] instead.
val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t
  • deprecated Use [decompose_lambda_assum] instead.
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct