package coq

  1. Overview
  2. Docs
package coq
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.

type types = t
type constr = t
type existential = t Constr.pexistential
type case_return = t Constr.pcase_return
type case_branch = t Constr.pcase_branch
type fixpoint = (t, t) Constr.pfixpoint
type cofixpoint = (t, t) Constr.pcofixpoint
type unsafe_judgment = (constr, types) Environ.punsafe_judgment
type unsafe_type_judgment = types Environ.punsafe_type_judgment
type named_declaration = (constr, types) Context.Named.Declaration.pt
type rel_declaration = (constr, types) Context.Rel.Declaration.pt
type named_context = (constr, types) Context.Named.pt
type rel_context = (constr, types) Context.Rel.pt
Universe variables
module ESorts : sig ... end
module EInstance : sig ... end
type case_invert = t Constr.pcase_invert
type case = (t, t, EInstance.t) Constr.pcase
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 Context.binder_annot * t * t
  4. | LetInType of Names.Name.t Context.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 : Sorts.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 Context.binder_annot * t * t) -> t
val mkLambda : (Names.Name.t Context.binder_annot * t * t) -> t
val mkLetIn : (Names.Name.t Context.binder_annot * t * t * t) -> t
val mkApp : (t * t array) -> t
val mkConst : Names.Constant.t -> t
val mkConstU : (Names.Constant.t * EInstance.t) -> t
val mkProj : (Names.Projection.t * t) -> t
val mkInd : Names.inductive -> t
val mkIndU : (Names.inductive * EInstance.t) -> t
val mkConstruct : Names.constructor -> t
val mkConstructU : (Names.constructor * EInstance.t) -> t
val mkConstructUi : ((Names.inductive * EInstance.t) * int) -> t
val mkCase : case -> t
val mkFix : (t, t) Constr.pfixpoint -> t
val mkCoFix : (t, t) Constr.pcofixpoint -> t
val mkArrow : t -> Sorts.relevance -> t -> t
val mkArrowR : t -> t -> t
val mkInt : Uint63.t -> t
val mkFloat : Float64.t -> t
val mkArray : (EInstance.t * t array * t * t) -> t
val mkRef : (Names.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 : Names.Id.t Context.binder_annot -> types -> constr -> constr
val mkNamedLetIn : Names.Id.t Context.binder_annot -> constr -> types -> constr -> constr
val mkNamedProd : Names.Id.t Context.binder_annot -> types -> types -> types
val mkNamedLambda_or_LetIn : named_declaration -> types -> types
val mkNamedProd_or_LetIn : named_declaration -> types -> types
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 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 : Evd.evar_map -> Names.GlobRef.t -> t -> bool
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 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 destProj : Evd.evar_map -> t -> Names.Projection.t * t
val destFix : Evd.evar_map -> t -> (t, t) Constr.pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t) Constr.pcofixpoint
val decompose_app : Evd.evar_map -> t -> t * t list
val decompose_lam : Evd.evar_map -> t -> (Names.Name.t Context.binder_annot * t) list * t

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

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

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

val decompose_lam_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_lam_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 compose_lam : (Names.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 -> (Names.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
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_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 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 -> 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 : (t, t) Constr.prec_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 identity_subst_val : Environ.named_context_val -> t list
val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Evd.evar_map * t
val is_global : Evd.evar_map -> Names.GlobRef.t -> t -> bool
  • deprecated Use [EConstr.isRefX] instead.
val expand_case : Environ.env -> Evd.evar_map -> case -> Constr.case_info * t * case_invert * t * t array
val annotate_case : Environ.env -> Evd.evar_map -> case -> Constr.case_info * EInstance.t * t array * (rel_context * 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.

val contract_case : Environ.env -> Evd.evar_map -> (Constr.case_info * t * case_invert * t * t array) -> case
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 of_case_invert : Constr.case_invert -> case_invert
val of_constr_array : Constr.t array -> t array
Unsafe operations
module Unsafe : sig ... end
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