package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module EConstrSource

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

Sourcetype types = t
Sourcetype constr = t
Sourcetype existential = t Constr.pexistential
Sourcetype case_return = t Constr.pcase_return
Sourcetype case_branch = t Constr.pcase_branch
Sourcetype fixpoint = (t, t) Constr.pfixpoint
Sourcetype cofixpoint = (t, t) Constr.pcofixpoint
Sourcetype unsafe_judgment = (constr, types) Environ.punsafe_judgment
Sourcetype unsafe_type_judgment = types Environ.punsafe_type_judgment
Sourcetype named_declaration = (constr, types) Context.Named.Declaration.pt
Sourcetype named_context = (constr, types) Context.Named.pt
Sourcetype rel_context = (constr, types) Context.Rel.pt
Universe variables
Sourcemodule ESorts : sig ... end
Sourcemodule EInstance : sig ... end
Sourcetype case_invert = t Constr.pcase_invert
Sourcetype 'a puniverses = 'a * EInstance.t
Destructors

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

Sourceval 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.

Sourceval to_constr_opt : Evd.evar_map -> t -> Constr.t option

Same as to_constr, but returns None if some unresolved evars remain

Sourcetype 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
Sourceval kind_of_type : Evd.evar_map -> t -> kind_of_type
Constructors

Construct a term from a view.

Sourceval 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
Sourceval mkRel : int -> t
Sourceval mkVar : Names.Id.t -> t
Sourceval mkEvar : t Constr.pexistential -> t
Sourceval mkSort : Sorts.t -> t
Sourceval mkSProp : t
Sourceval mkProp : t
Sourceval mkSet : t
Sourceval mkType : Univ.Universe.t -> t
Sourceval mkCast : (t * Constr.cast_kind * t) -> t
Sourceval mkLambda : (Names.Name.t Context.binder_annot * t * t) -> t
Sourceval mkLetIn : (Names.Name.t Context.binder_annot * t * t * t) -> t
Sourceval mkApp : (t * t array) -> t
Sourceval mkConst : Names.Constant.t -> t
Sourceval mkConstU : (Names.Constant.t * EInstance.t) -> t
Sourceval mkProj : (Names.Projection.t * t) -> t
Sourceval mkInd : Names.inductive -> t
Sourceval mkIndU : (Names.inductive * EInstance.t) -> t
Sourceval mkConstruct : Names.constructor -> t
Sourceval mkConstructU : (Names.constructor * EInstance.t) -> t
Sourceval mkConstructUi : ((Names.inductive * EInstance.t) * int) -> t
Sourceval mkCase : case -> t
Sourceval mkFix : (t, t) Constr.pfixpoint -> t
Sourceval mkCoFix : (t, t) Constr.pcofixpoint -> t
Sourceval mkArrow : t -> Sorts.relevance -> t -> t
Sourceval mkArrowR : t -> t -> t
Sourceval mkInt : Uint63.t -> t
Sourceval mkFloat : Float64.t -> t
Sourceval mkArray : (EInstance.t * t array * t * t) -> t
Sourceval type1 : t
Sourceval applist : (t * t list) -> t
Sourceval applistc : t -> t list -> t
Sourceval mkProd_or_LetIn : rel_declaration -> t -> t
Sourceval mkLambda_or_LetIn : rel_declaration -> t -> t
Sourceval it_mkProd_or_LetIn : t -> rel_context -> t
Sourceval it_mkLambda_or_LetIn : t -> rel_context -> t
Sourceval mkNamedLambda_or_LetIn : named_declaration -> types -> types
Sourceval mkNamedProd_or_LetIn : named_declaration -> types -> types
Simple case analysis
Sourceval isRel : Evd.evar_map -> t -> bool
Sourceval isVar : Evd.evar_map -> t -> bool
Sourceval isInd : Evd.evar_map -> t -> bool
Sourceval isRef : Evd.evar_map -> t -> bool
Sourceval isEvar : Evd.evar_map -> t -> bool
Sourceval isMeta : Evd.evar_map -> t -> bool
Sourceval isSort : Evd.evar_map -> t -> bool
Sourceval isCast : Evd.evar_map -> t -> bool
Sourceval isApp : Evd.evar_map -> t -> bool
Sourceval isLambda : Evd.evar_map -> t -> bool
Sourceval isLetIn : Evd.evar_map -> t -> bool
Sourceval isProd : Evd.evar_map -> t -> bool
Sourceval isConst : Evd.evar_map -> t -> bool
Sourceval isConstruct : Evd.evar_map -> t -> bool
Sourceval isFix : Evd.evar_map -> t -> bool
Sourceval isCoFix : Evd.evar_map -> t -> bool
Sourceval isCase : Evd.evar_map -> t -> bool
Sourceval isProj : Evd.evar_map -> t -> bool
Sourceval isType : Evd.evar_map -> constr -> bool
Sourceval destArity : Evd.evar_map -> types -> arity
Sourceval isArity : Evd.evar_map -> t -> bool
Sourceval isVarId : Evd.evar_map -> Names.Id.t -> t -> bool
Sourceval isRelN : Evd.evar_map -> int -> t -> bool
Sourceval isRefX : Evd.evar_map -> Names.GlobRef.t -> t -> bool
Sourceval destRel : Evd.evar_map -> t -> int
Sourceval destVar : Evd.evar_map -> t -> Names.Id.t
Sourceval destSort : Evd.evar_map -> t -> ESorts.t
Sourceval destCast : Evd.evar_map -> t -> t * Constr.cast_kind * t
Sourceval destApp : Evd.evar_map -> t -> t * t array
Sourceval destCase : Evd.evar_map -> t -> case
Sourceval destProj : Evd.evar_map -> t -> Names.Projection.t * t
Sourceval destFix : Evd.evar_map -> t -> (t, t) Constr.pfixpoint
Sourceval destCoFix : Evd.evar_map -> t -> (t, t) Constr.pcofixpoint
Sourceval decompose_app : Evd.evar_map -> t -> t * t list
Sourceval 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.

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

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

Sourceval 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.

Sourceval 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.

Sourceval compose_lam : (Names.Name.t Context.binder_annot * t) list -> t -> t
Sourceval to_lambda : Evd.evar_map -> int -> t -> t
Sourceval decompose_prod : Evd.evar_map -> t -> (Names.Name.t Context.binder_annot * t) list * t
Sourceval decompose_prod_assum : Evd.evar_map -> t -> rel_context * t
Sourceval decompose_prod_n_assum : Evd.evar_map -> int -> t -> rel_context * t
Sourceval existential_type : Evd.evar_map -> existential -> types
Sourceval whd_evar : Evd.evar_map -> constr -> constr
Equality
Sourceval eq_constr : Evd.evar_map -> t -> t -> bool
Sourceval eq_constr_nounivs : Evd.evar_map -> t -> t -> bool
Sourceval eq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
Sourceval leq_constr_universes : Environ.env -> Evd.evar_map -> ?nargs:int -> t -> t -> UnivProblem.Set.t option
Sourceval 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.

Sourceval compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
Iterators
Sourceval map : Evd.evar_map -> (t -> t) -> t -> t
Sourceval map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
Sourceval map_branches : (t -> t) -> case_branch array -> case_branch array
Sourceval map_return_predicate : (t -> t) -> case_return -> case_return
Sourceval iter : Evd.evar_map -> (t -> unit) -> t -> unit
Sourceval iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
Sourceval iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
Sourceval fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
Sourceval fold_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> t -> 'b) -> 'a -> 'b -> t -> 'b
Sourceval 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
Sourcemodule Vars : sig ... end

See vars.mli for the documentation of the functions below

Environment handling
Sourceval push_rel_context : rel_context -> Environ.env -> Environ.env
Sourceval push_named_context : named_context -> Environ.env -> Environ.env
Sourceval rel_context : Environ.env -> rel_context
Sourceval named_context : Environ.env -> named_context
Sourceval val_of_named_context : named_context -> Environ.named_context_val
Sourceval named_context_of_val : Environ.named_context_val -> named_context
Sourceval lookup_rel : int -> Environ.env -> rel_declaration
Sourceval map_rel_context_in_env : (Environ.env -> constr -> constr) -> Environ.env -> rel_context -> rel_context
Sourceval identity_subst_val : Environ.named_context_val -> t list
Sourceval fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Evd.evar_map * t
Sourceval is_global : Evd.evar_map -> Names.GlobRef.t -> t -> bool
  • deprecated Use [EConstr.isRefX] instead.
Sourceval expand_case : Environ.env -> Evd.evar_map -> case -> Constr.case_info * t * case_invert * t * t array
Sourceval 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

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

Sourceval contract_case : Environ.env -> Evd.evar_map -> (Constr.case_info * t * case_invert * t * t array) -> case
Extra
Sourceval of_existential : Constr.existential -> existential
Sourceval of_named_context : Constr.named_context -> named_context
Sourceval of_rel_context : Constr.rel_context -> rel_context
Sourceval of_case_invert : Constr.case_invert -> case_invert
Sourceval of_constr_array : Constr.t array -> t array
Unsafe operations
Sourcemodule 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