package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
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
val to_constr : Evd.evar_map -> t -> Constr.t
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 mkProp : t
val mkSet : t
val mkType : Univ.universe -> t
val mkCast : (t * Constr.cast_kind * t) -> t
val mkProd : (Names.Name.t * t * t) -> t
val mkLambda : (Names.Name.t * t * t) -> t
val mkLetIn : (Names.Name.t * t * t * t) -> t
val mkApp : (t * t array) -> t
val mkConst : Names.constant -> t
val mkConstU : (Names.constant * EInstance.t) -> t
val mkProj : (Names.projection * 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 -> t -> t
val applist : (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 -> types -> constr -> constr
val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr
val mkNamedProd : Names.Id.t -> 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 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 destProd : Evd.evar_map -> t -> Names.Name.t * types * types
val destLambda : Evd.evar_map -> t -> Names.Name.t * types * t
val destLetIn : Evd.evar_map -> t -> Names.Name.t * t * types * t
val destApp : Evd.evar_map -> t -> t * t array
val destConst : Evd.evar_map -> t -> Names.constant * 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
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 * 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 * t) list -> t -> t
val to_lambda : Evd.evar_map -> int -> t -> t
val decompose_prod : Evd.evar_map -> t -> (Names.Name.t * 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 : Evd.evar_map -> t -> t -> Universes.universe_constraints option
val leq_constr_universes : Evd.evar_map -> t -> t -> Universes.universe_constraints option
val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.universe_constraints option
val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
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 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
module Vars : sig ... end
val push_rel_context : rel_context -> 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 fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t
val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
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