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 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 -> 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 -> 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 -> 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 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 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.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 * 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 : 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_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
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