package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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_relevance : Sorts.relevance;
  6. ci_pp_info : case_printing;
}
type (!'constr, !'univs) case_invert =
  1. | NoInvert
  2. | CaseInvert of {
    1. univs : 'univs;
    2. args : 'constr array;
    }
type t
type constr = t
type types = constr
val mkRel : int -> constr
val mkVar : Names.Id.t -> constr
val mkInt : Uint63.t -> constr
val mkArray : (Univ.Instance.t * constr array * constr * types) -> constr
val mkFloat : Float64.t -> constr
val mkMeta : metavariable -> constr
type existential = Evar.t * constr list
val mkEvar : existential -> constr
val mkSort : Sorts.t -> types
val mkSProp : 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 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
type (!'constr, !'types) prec_declaration = Names.Name.t Context.binder_annot 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 list
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 Context.binder_annot * 'types * 'types
  8. | Lambda of Names.Name.t Context.binder_annot * 'types * 'constr
  9. | LetIn of Names.Name.t Context.binder_annot * '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, 'univs) case_invert * 'constr * 'constr array
  15. | Fix of ('constr, 'types) pfixpoint
  16. | CoFix of ('constr, 'types) pcofixpoint
  17. | Proj of Names.Projection.t * 'constr
  18. | Int of Uint63.t
  19. | Float of Float64.t
  20. | Array of 'univs * 'constr array * 'constr * 'types
val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> 'v -> ('v, 'v, 'sort, 'univs) kind_of_term
val isRel : constr -> bool
val isRelN : int -> constr -> bool
val isVar : constr -> bool
val isVarId : Names.Id.t -> constr -> bool
val isRef : constr -> bool
val isRefX : Names.GlobRef.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 destApp : constr -> constr * constr array
val decompose_app : constr -> constr * constr list
val decompose_appvect : constr -> constr * constr array
val destEvar : constr -> existential
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 exliftn : Esubst.lift -> constr -> constr
val liftn : int -> int -> constr -> constr
val lift : int -> constr -> constr
val map_under_context : (constr -> constr) -> int -> constr -> constr
val map_branches : (constr -> constr) -> case_info -> constr array -> constr array
val map_return_predicate : (constr -> constr) -> case_info -> constr -> constr
val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr
val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array
val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr
val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array
val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
val fold_with_full_binders : (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a
val map : (constr -> constr) -> constr -> constr
val map_invert : ('a -> 'a) -> ('a, 'b) case_invert -> ('a, 'b) case_invert
val map_user_view : (constr -> constr) -> constr -> constr
val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
val fold_map_invert : ('a -> 'b -> 'a * 'b) -> 'a -> ('b, 'c) case_invert -> 'a * ('b, 'c) case_invert
val map_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
val iter : (constr -> unit) -> constr -> unit
val iter_invert : ('a -> unit) -> ('a, 'b) case_invert -> 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 constr_compare_fn = int -> 'constr -> 'constr -> bool
type !'univs instance_compare_fn = (Names.GlobRef.t * int) option -> 'univs -> 'univs -> bool
val compare_head_gen_leq_with : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> 'univs instance_compare_fn -> ('sort -> 'sort -> bool) -> 'v constr_compare_fn -> 'v constr_compare_fn -> 'v constr_compare_fn
val compare_head_gen_with : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> 'univs instance_compare_fn -> ('sort -> 'sort -> bool) -> 'v constr_compare_fn -> 'v constr_compare_fn
val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a, 'b) case_invert -> ('a, 'b) case_invert -> bool
val hash : constr -> int
val case_info_hash : case_info -> int
val hcons : constr -> constr
val debug_print : constr -> Pp.t
val debug_print_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t