coq 8.10.2 · OCaml Package

type pconstant = Names.Constant.t Univ.puniverses

type pinductive = Names.inductive Univ.puniverses

type pconstructor = Names.constructor Univ.puniverses

type metavariable = int

type case_style =

| LetStyle
| IfStyle
| LetPatternStyle
| MatchStyle
| RegularStyle

type case_printing = {

ind_tags : bool list;
cstr_tags : bool list array;
style : case_style;

}

type case_info = {

ci_ind : Names.inductive;
ci_npar : int;
ci_cstr_ndecls : int array;
ci_cstr_nargs : int array;
ci_relevance : Sorts.relevance;
ci_pp_info : case_printing;

}

type t

type constr = t

type types = constr

val mkRel : int -> constr

val mkVar : Names.Id.t -> constr

val mkInt : Uint63.t -> constr

val mkMeta : metavariable -> constr

type existential = Evar.t * constr array

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 =

| VMcast
| NATIVEcast
| DEFAULTcast
| REVERTcast

val mkCast : (constr * cast_kind * constr) -> constr

val mkProd : (Names.Name.t Context.binder_annot * types * types) -> types

val mkLambda : (Names.Name.t Context.binder_annot * types * constr) -> constr

val mkLetIn : 
  (Names.Name.t Context.binder_annot * 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 mkRef : Names.GlobRef.t Univ.puniverses -> constr

val mkCase : (case_info * constr * constr * constr array) -> 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 array

type (!'constr, !'types, !'sort, !'univs) kind_of_term =

| Rel of int
| Var of Names.Id.t
| Meta of metavariable
| Evar of 'constr pexistential
| Sort of 'sort
| Cast of 'constr * cast_kind * 'types
| Prod of Names.Name.t Context.binder_annot * 'types * 'types
| Lambda of Names.Name.t Context.binder_annot * 'types * 'constr
| LetIn of Names.Name.t Context.binder_annot * 'constr * 'types * 'constr
| App of 'constr * 'constr array
| Const of Names.Constant.t * 'univs
| Ind of Names.inductive * 'univs
| Construct of Names.constructor * 'univs
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
| Proj of Names.Projection.t * 'constr
| Int of Uint63.t

val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term

val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr

val kind_nocast_gen : 
  ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) ->
  'v ->
  ('v, 'v, 'sort, 'univs) kind_of_term

val kind_nocast : 
  constr ->
  (constr, types, Sorts.t, Univ.Instance.t) kind_of_term

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 Context.binder_annot * types * types

val destLambda : constr -> Names.Name.t Context.binder_annot * types * constr

val destLetIn : 
  constr ->
  Names.Name.t Context.binder_annot * constr * types * constr

val destApp : constr -> constr * constr array

val decompose_app : constr -> constr * constr list

val decompose_appvect : constr -> constr * constr array

val destConst : constr -> Names.Constant.t Univ.puniverses

val destEvar : constr -> existential

val destInd : constr -> Names.inductive Univ.puniverses

val destConstruct : constr -> Names.constructor Univ.puniverses

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 destRef : constr -> Names.GlobRef.t Univ.puniverses

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 map : (constr -> constr) -> constr -> constr

val map_user_view : (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 constr_compare_fn = int -> 'constr -> 'constr -> bool

val compare_head : constr constr_compare_fn -> constr constr_compare_fn

type !'univs instance_compare_fn =
  Names.GlobRef.t ->
  int ->
  'univs ->
  'univs ->
  bool

val compare_head_gen : 
  Univ.Instance.t instance_compare_fn ->
  (Sorts.t -> Sorts.t -> bool) ->
  constr constr_compare_fn ->
  constr constr_compare_fn

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 compare_head_gen_leq : 
  Univ.Instance.t instance_compare_fn ->
  (Sorts.t -> Sorts.t -> bool) ->
  constr constr_compare_fn ->
  constr constr_compare_fn ->
  constr constr_compare_fn

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

package coq