package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = Evd.econstr
type types = t
type constr = t
type existential = t Constr.pexistential
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
module ESorts : sig ... end
module EInstance : sig ... end
type !'a puniverses = 'a * EInstance.t
val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
val to_constr_opt : Evd.evar_map -> t -> Constr.t option
val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
val of_constr : Constr.t -> t
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 : (Constr.case_info * t * t * t array) -> 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 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
val isRel : Evd.evar_map -> t -> bool
val isVar : Evd.evar_map -> t -> bool
val isInd : 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 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 -> Constr.case_info * t * t * t array
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
val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t
val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t
val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t
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
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 -> t -> t -> UnivProblem.Set.t option
val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option
val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
val map : Evd.evar_map -> (t -> t) -> t -> t
val map_user_view : Evd.evar_map -> (t -> t) -> t -> t
val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
val map_under_context : (t -> t) -> int -> t -> t
val map_branches : (t -> t) -> Constr.case_info -> t array -> t array
val map_return_predicate : (t -> t) -> Constr.case_info -> t -> t
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 : 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 universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
module Vars : sig ... end
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 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
val of_existential : Constr.existential -> existential
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