package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a puniverses = 'a Univ.puniverses
  • deprecated use Univ.puniverses
type existential_key = Evar.t
  • deprecated use Evar.t
type metavariable = int
type case_style =
  1. | LetStyle
  2. | IfStyle
  3. | LetPatternStyle
  4. | MatchStyle
  5. | RegularStyle
type case_printing = {
  1. ind_tags : bool list;
  2. cstr_tags : bool list array;
  3. style : case_style;
}
type case_info = {
  1. ci_ind : Names.inductive;
  2. ci_npar : int;
  3. ci_cstr_ndecls : int array;
  4. ci_cstr_nargs : int array;
  5. ci_pp_info : case_printing;
}
type t
type constr = t
type types = constr
val mkRel : int -> constr
val mkVar : Names.Id.t -> constr
val mkMeta : metavariable -> constr
type existential = Evar.t * constr array
val mkEvar : existential -> constr
val mkSort : Sorts.t -> types
val mkProp : types
val mkSet : types
val mkType : Univ.Universe.t -> types
type cast_kind =
  1. | VMcast
  2. | NATIVEcast
  3. | DEFAULTcast
  4. | REVERTcast
val mkCast : (constr * cast_kind * constr) -> constr
val mkProd : (Names.Name.t * types * types) -> types
val mkLambda : (Names.Name.t * types * constr) -> constr
val mkLetIn : (Names.Name.t * constr * types * constr) -> constr
val mkApp : (constr * constr array) -> constr
val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses
val mkConst : Names.Constant.t -> constr
val mkConstU : pconstant -> constr
val mkProj : (Names.Projection.t * constr) -> constr
val mkInd : Names.inductive -> constr
val mkIndU : pinductive -> constr
val mkConstruct : Names.constructor -> constr
val mkConstructU : pconstructor -> constr
val mkConstructUi : (pinductive * int) -> constr
val mkCase : (case_info * constr * constr * constr array) -> constr
type (!'constr, !'types) prec_declaration = Names.Name.t array * 'types array * 'constr array
type (!'constr, !'types) pfixpoint = (int array * int) * ('constr, 'types) prec_declaration
type (!'constr, !'types) pcofixpoint = int * ('constr, 'types) prec_declaration
type rec_declaration = (constr, types) prec_declaration
type fixpoint = (constr, types) pfixpoint
val mkFix : fixpoint -> constr
type cofixpoint = (constr, types) pcofixpoint
val mkCoFix : cofixpoint -> constr
type !'constr pexistential = Evar.t * 'constr array
type (!'constr, !'types, !'sort, !'univs) kind_of_term =
  1. | Rel of int
  2. | Var of Names.Id.t
  3. | Meta of metavariable
  4. | Evar of 'constr pexistential
  5. | Sort of 'sort
  6. | Cast of 'constr * cast_kind * 'types
  7. | Prod of Names.Name.t * 'types * 'types
  8. | Lambda of Names.Name.t * 'types * 'constr
  9. | LetIn of Names.Name.t * 'constr * 'types * 'constr
  10. | App of 'constr * 'constr array
  11. | Const of Names.Constant.t * 'univs
  12. | Ind of Names.inductive * 'univs
  13. | Construct of Names.constructor * 'univs
  14. | Case of case_info * 'constr * 'constr * 'constr array
  15. | Fix of ('constr, 'types) pfixpoint
  16. | CoFix of ('constr, 'types) pcofixpoint
  17. | Proj of Names.Projection.t * 'constr
val isRel : constr -> bool
val isRelN : int -> constr -> bool
val isVar : constr -> bool
val isVarId : Names.Id.t -> constr -> bool
val isInd : constr -> bool
val isEvar : constr -> bool
val isMeta : constr -> bool
val isEvar_or_Meta : constr -> bool
val isSort : constr -> bool
val isCast : constr -> bool
val isApp : constr -> bool
val isLambda : constr -> bool
val isLetIn : constr -> bool
val isProd : constr -> bool
val isConst : constr -> bool
val isConstruct : constr -> bool
val isFix : constr -> bool
val isCoFix : constr -> bool
val isCase : constr -> bool
val isProj : constr -> bool
val is_Prop : constr -> bool
val is_Set : constr -> bool
val isprop : constr -> bool
val is_Type : constr -> bool
val iskind : constr -> bool
val is_small : Sorts.t -> bool
exception DestKO
val destRel : constr -> int
val destMeta : constr -> metavariable
val destVar : constr -> Names.Id.t
val destSort : constr -> Sorts.t
val destCast : constr -> constr * cast_kind * constr
val destProd : types -> Names.Name.t * types * types
val destLambda : constr -> Names.Name.t * types * constr
val destLetIn : constr -> Names.Name.t * constr * types * constr
val destApp : constr -> constr * constr array
val decompose_app : constr -> constr * constr list
val decompose_appvect : constr -> constr * constr array
val destEvar : constr -> existential
val destCase : constr -> case_info * constr * constr * constr array
val destProj : constr -> Names.Projection.t * constr
val destFix : constr -> fixpoint
val destCoFix : constr -> cofixpoint
val equal : constr -> constr -> bool
val eq_constr_univs : constr UGraph.check_function
val leq_constr_univs : constr UGraph.check_function
val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained
val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained
val eq_constr_nounivs : constr -> constr -> bool
val compare : constr -> constr -> int
type rel_declaration = (constr, types) Context.Rel.Declaration.pt
type named_declaration = (constr, types) Context.Named.Declaration.pt
type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
type rel_context = rel_declaration list
type named_context = named_declaration list
type compacted_context = compacted_declaration list
val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
val map : (constr -> constr) -> constr -> constr
val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
val map_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
val iter : (constr -> unit) -> constr -> unit
val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
type constr_compare_fn = int -> constr -> constr -> bool
val compare_head : constr_compare_fn -> constr_compare_fn
type instance_compare_fn = Names.GlobRef.t -> int -> Univ.Instance.t -> Univ.Instance.t -> bool
val compare_head_gen : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> constr_compare_fn -> constr_compare_fn
val compare_head_gen_leq : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> constr_compare_fn -> constr_compare_fn -> constr_compare_fn
val hash : constr -> int
val case_info_hash : case_info -> int
val hcons : constr -> constr