coq 8.7.2 · OCaml Package

type !'a puniverses = 'a Univ.puniverses

type pconstant = Names.constant puniverses

type pinductive = Names.inductive puniverses

type pconstructor = Names.constructor puniverses

type existential_key = Evar.t

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_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 = existential_key * constr array

val mkEvar : existential -> constr

val mkSort : Sorts.t -> types

val mkProp : types

val mkSet : types

val mkType : Univ.universe -> types

type cast_kind =

| VMcast
| NATIVEcast
| DEFAULTcast
| 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 puniverses -> 'b puniverses

val mkConst : Names.constant -> constr

val mkConstU : pconstant -> constr

val mkProj : (Names.projection * 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 rec_declaration = Names.Name.t array * types array * constr array

type fixpoint = (int array * int) * rec_declaration

val mkFix : fixpoint -> constr

type cofixpoint = int * rec_declaration

val mkCoFix : cofixpoint -> constr

type !'constr pexistential = existential_key * 'constr array

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 (!'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 * 'types * 'types
| Lambda of Names.Name.t * 'types * 'constr
| LetIn of Names.Name.t * 'constr * 'types * 'constr
| App of 'constr * 'constr array
| Const of Names.constant * '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 * 'constr

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 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

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

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

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

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

val compare_head_gen_leq : 
  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
  (Sorts.t -> Sorts.t -> bool) ->
  (constr -> constr -> bool) ->
  (constr -> constr -> bool) ->
  constr ->
  constr ->
  bool

val hash : constr -> int

val case_info_hash : case_info -> int

val hcons : constr -> constr

type values

package coq