coq 8.8.1 · OCaml Package

type !'a puniverses = 'a Univ.puniverses

deprecated use Univ.puniverses

type pconstant = Names.Constant.t Univ.puniverses

type pinductive = Names.inductive Univ.puniverses

type pconstructor = Names.constructor Univ.puniverses

type existential_key = Evar.t

deprecated use 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 = 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 =

| 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 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 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 = Evar.t * '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.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

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 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 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 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 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.global_reference ->
  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_with : 
  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
  (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
  instance_compare_fn ->
  (Sorts.t -> Sorts.t -> bool) ->
  constr_compare_fn ->
  constr_compare_fn ->
  constr_compare_fn

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

package coq