coq 8.8.1 · OCaml Package

exception DestKO

val isRel : Constr.constr -> bool

deprecated Alias for [Constr.isRel]

val isRelN : int -> Constr.constr -> bool

deprecated Alias for [Constr.isRelN]

val isVar : Constr.constr -> bool

deprecated Alias for [Constr.isVar]

val isVarId : Names.Id.t -> Constr.constr -> bool

deprecated Alias for [Constr.isVarId]

val isInd : Constr.constr -> bool

deprecated Alias for [Constr.isInd]

val isEvar : Constr.constr -> bool

deprecated Alias for [Constr.isEvar]

val isMeta : Constr.constr -> bool

deprecated Alias for [Constr.isMeta]

val isEvar_or_Meta : Constr.constr -> bool

deprecated Alias for [Constr.isEvar_or_Meta]

val isSort : Constr.constr -> bool

deprecated Alias for [Constr.isSort]

val isCast : Constr.constr -> bool

deprecated Alias for [Constr.isCast]

val isApp : Constr.constr -> bool

deprecated Alias for [Constr.isApp]

val isLambda : Constr.constr -> bool

deprecated Alias for [Constr.isLambda]

val isLetIn : Constr.constr -> bool

deprecated Alias for [Constr.isletIn]

val isProd : Constr.constr -> bool

deprecated Alias for [Constr.isProp]

val isConst : Constr.constr -> bool

deprecated Alias for [Constr.isConst]

val isConstruct : Constr.constr -> bool

deprecated Alias for [Constr.isConstruct]

val isFix : Constr.constr -> bool

deprecated Alias for [Constr.isFix]

val isCoFix : Constr.constr -> bool

deprecated Alias for [Constr.isCoFix]

val isCase : Constr.constr -> bool

deprecated Alias for [Constr.isCase]

val isProj : Constr.constr -> bool

deprecated Alias for [Constr.isProj]

val is_Prop : Constr.constr -> bool

deprecated Alias for [Constr.is_Prop]

val is_Set : Constr.constr -> bool

deprecated Alias for [Constr.is_Set]

val isprop : Constr.constr -> bool

deprecated Alias for [Constr.isprop]

val is_Type : Constr.constr -> bool

deprecated Alias for [Constr.is_Type]

val iskind : Constr.constr -> bool

deprecated Alias for [Constr.is_kind]

val is_small : Sorts.t -> bool

deprecated Alias for [Constr.is_small]

val destRel : Constr.constr -> int

deprecated Alias for [Constr.destRel]

val destMeta : Constr.constr -> Constr.metavariable

deprecated Alias for [Constr.destMeta]

val destVar : Constr.constr -> Names.Id.t

deprecated Alias for [Constr.destVar]

val destSort : Constr.constr -> Sorts.t

deprecated Alias for [Constr.destSort]

val destCast : 
  Constr.constr ->
  Constr.constr * Constr.cast_kind * Constr.constr

deprecated Alias for [Constr.destCast]

val destProd : Constr.types -> Names.Name.t * Constr.types * Constr.types

deprecated Alias for [Constr.destProd]

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

deprecated Alias for [Constr.destLambda]

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

deprecated Alias for [Constr.destLetIn]

val destApp : Constr.constr -> Constr.constr * Constr.constr array

deprecated Alias for [Constr.destApp]

val destApplication : Constr.constr -> Constr.constr * Constr.constr array

deprecated Alias for [Constr.destApplication]

val decompose_app : Constr.constr -> Constr.constr * Constr.constr list

deprecated Alias for [Constr.decompose_app]

val decompose_appvect : Constr.constr -> Constr.constr * Constr.constr array

deprecated Alias for [Constr.decompose_appvect]

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

deprecated Alias for [Constr.destConst]

val destEvar : Constr.constr -> Constr.existential

deprecated Alias for [Constr.destEvar]

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

deprecated Alias for [Constr.destInd]

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

deprecated Alias for [Constr.destConstruct]

val destCase : 
  Constr.constr ->
  Constr.case_info * Constr.constr * Constr.constr * Constr.constr array

deprecated Alias for [Constr.destCase]

val destProj : Constr.constr -> Names.Projection.t * Constr.constr

deprecated Alias for [Constr.destProj]

val destFix : Constr.constr -> Constr.fixpoint

deprecated Alias for [Constr.destFix]

val destCoFix : Constr.constr -> Constr.cofixpoint

deprecated Alias for [Constr.destCoFix]

val mkArrow : Constr.types -> Constr.types -> Constr.constr

val mkNamedLambda : 
  Names.Id.t ->
  Constr.types ->
  Constr.constr ->
  Constr.constr

val mkNamedLetIn : 
  Names.Id.t ->
  Constr.constr ->
  Constr.types ->
  Constr.constr ->
  Constr.constr

val mkNamedProd : Names.Id.t -> Constr.types -> Constr.types -> Constr.types

val mkProd_or_LetIn : Context.Rel.Declaration.t -> Constr.types -> Constr.types

val mkProd_wo_LetIn : Context.Rel.Declaration.t -> Constr.types -> Constr.types

val mkNamedProd_or_LetIn : 
  Context.Named.Declaration.t ->
  Constr.types ->
  Constr.types

val mkNamedProd_wo_LetIn : 
  Context.Named.Declaration.t ->
  Constr.types ->
  Constr.types

val mkLambda_or_LetIn : 
  Context.Rel.Declaration.t ->
  Constr.constr ->
  Constr.constr

val mkNamedLambda_or_LetIn : 
  Context.Named.Declaration.t ->
  Constr.constr ->
  Constr.constr

val applist : (Constr.constr * Constr.constr list) -> Constr.constr

val applistc : Constr.constr -> Constr.constr list -> Constr.constr

val appvect : (Constr.constr * Constr.constr array) -> Constr.constr

val appvectc : Constr.constr -> Constr.constr array -> Constr.constr

val prodn : 
  int ->
  (Names.Name.t * Constr.constr) list ->
  Constr.constr ->
  Constr.constr

val compose_prod : 
  (Names.Name.t * Constr.constr) list ->
  Constr.constr ->
  Constr.constr

val lamn : 
  int ->
  (Names.Name.t * Constr.constr) list ->
  Constr.constr ->
  Constr.constr

val compose_lam : 
  (Names.Name.t * Constr.constr) list ->
  Constr.constr ->
  Constr.constr

val to_lambda : int -> Constr.constr -> Constr.constr

val to_prod : int -> Constr.constr -> Constr.constr

val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr

val it_mkProd_or_LetIn : Constr.types -> Context.Rel.t -> Constr.types

val lambda_applist : Constr.constr -> Constr.constr list -> Constr.constr

val lambda_appvect : Constr.constr -> Constr.constr array -> Constr.constr

val lambda_applist_assum : 
  int ->
  Constr.constr ->
  Constr.constr list ->
  Constr.constr

val lambda_appvect_assum : 
  int ->
  Constr.constr ->
  Constr.constr array ->
  Constr.constr

val prod_appvect : Constr.types -> Constr.constr array -> Constr.types

val prod_applist : Constr.types -> Constr.constr list -> Constr.types

val prod_appvect_assum : 
  int ->
  Constr.types ->
  Constr.constr array ->
  Constr.types

val prod_applist_assum : 
  int ->
  Constr.types ->
  Constr.constr list ->
  Constr.types

val decompose_prod : 
  Constr.constr ->
  (Names.Name.t * Constr.constr) list * Constr.constr

val decompose_lam : 
  Constr.constr ->
  (Names.Name.t * Constr.constr) list * Constr.constr

val decompose_prod_n : 
  int ->
  Constr.constr ->
  (Names.Name.t * Constr.constr) list * Constr.constr

val decompose_lam_n : 
  int ->
  Constr.constr ->
  (Names.Name.t * Constr.constr) list * Constr.constr

val decompose_prod_assum : Constr.types -> Context.Rel.t * Constr.types

val decompose_lam_assum : Constr.constr -> Context.Rel.t * Constr.constr

val decompose_prod_n_assum : 
  int ->
  Constr.types ->
  Context.Rel.t * Constr.types

val decompose_lam_n_assum : 
  int ->
  Constr.constr ->
  Context.Rel.t * Constr.constr

val decompose_lam_n_decls : 
  int ->
  Constr.constr ->
  Context.Rel.t * Constr.constr

val prod_assum : Constr.types -> Context.Rel.t

val lam_assum : Constr.constr -> Context.Rel.t

val prod_n_assum : int -> Constr.types -> Context.Rel.t

val lam_n_assum : int -> Constr.constr -> Context.Rel.t

val strip_prod : Constr.types -> Constr.types

val strip_lam : Constr.constr -> Constr.constr

val strip_prod_n : int -> Constr.types -> Constr.types

val strip_lam_n : int -> Constr.constr -> Constr.constr

val strip_prod_assum : Constr.types -> Constr.types

val strip_lam_assum : Constr.constr -> Constr.constr

type arity = Context.Rel.t * Sorts.t

val mkArity : arity -> Constr.types

val destArity : Constr.types -> arity

val isArity : Constr.types -> bool

type (!'constr, !'types) kind_of_type =

| SortType of Sorts.t
| CastType of 'types * 'types
| ProdType of Names.Name.t * 'types * 'types
| LetInType of Names.Name.t * 'constr * 'types * 'types
| AtomicType of 'constr * 'constr array

val kind_of_type : Constr.types -> (Constr.constr, Constr.types) kind_of_type

val set_sort : Sorts.t

deprecated Alias for Sorts.set

val prop_sort : Sorts.t

deprecated Alias for Sorts.prop

val type1_sort : Sorts.t

deprecated Alias for Sorts.type1

val sorts_ord : Sorts.t -> Sorts.t -> int

deprecated Alias for Sorts.compare

val is_prop_sort : Sorts.t -> bool

deprecated Alias for Sorts.is_prop

val family_of_sort : Sorts.t -> Sorts.family

deprecated Alias for Sorts.family

val mkRel : int -> Constr.constr

deprecated Alias for Constr.mkRel

val mkVar : Names.Id.t -> Constr.constr

deprecated Alias for Constr.mkVar

val mkMeta : Constr.metavariable -> Constr.constr

deprecated Alias for Constr.mkMeta

val mkEvar : Constr.existential -> Constr.constr

deprecated Alias for Constr.mkEvar

val mkSort : Sorts.t -> Constr.types

deprecated Alias for Constr.mkSort

val mkProp : Constr.types

deprecated Alias for Constr.mkProp

val mkSet : Constr.types

deprecated Alias for Constr.mkSet

val mkType : Univ.Universe.t -> Constr.types

deprecated Alias for Constr.mkType

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

deprecated Alias for Constr

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

deprecated Alias for Constr

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

deprecated Alias for Constr

val mkLetIn : 
  (Names.Name.t * Constr.constr * Constr.types * Constr.constr) ->
  Constr.constr

deprecated Alias for Constr

val mkApp : (Constr.constr * Constr.constr array) -> Constr.constr

deprecated Alias for Constr

val mkConst : Names.Constant.t -> Constr.constr

deprecated Alias for Constr

val mkProj : (Names.Projection.t * Constr.constr) -> Constr.constr

deprecated Alias for Constr

val mkInd : Names.inductive -> Constr.constr

deprecated Alias for Constr

val mkConstruct : Names.constructor -> Constr.constr

deprecated Alias for Constr

val mkConstU : Names.Constant.t Univ.puniverses -> Constr.constr

deprecated Alias for Constr

val mkIndU : Names.inductive Univ.puniverses -> Constr.constr

deprecated Alias for Constr

val mkConstructU : Names.constructor Univ.puniverses -> Constr.constr

deprecated Alias for Constr

val mkConstructUi : (Constr.pinductive * int) -> Constr.constr

deprecated Alias for Constr

val mkCase : 
  (Constr.case_info * Constr.constr * Constr.constr * Constr.constr array) ->
  Constr.constr

deprecated Alias for Constr.mkCase

val mkFix : Constr.fixpoint -> Constr.constr

deprecated Alias for Constr.mkFix

val mkCoFix : Constr.cofixpoint -> Constr.constr

deprecated Alias for Constr.mkCoFix

val eq_constr : Constr.constr -> Constr.constr -> bool

deprecated Alias for Constr.equal

val eq_constr_univs : Constr.constr UGraph.check_function

deprecated Alias for Constr.eq_constr_univs

val leq_constr_univs : Constr.constr UGraph.check_function

deprecated Alias for Constr.leq_constr_univs

val eq_constr_nounivs : Constr.constr -> Constr.constr -> bool

deprecated Alias for Constr.qe_constr_nounivs

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

deprecated Alias for Constr.kind

val compare : Constr.constr -> Constr.constr -> int

deprecated Alias for [Constr.compare]

val constr_ord : Constr.constr -> Constr.constr -> int

deprecated Alias for [Term.compare]

val fold_constr : ('a -> Constr.constr -> 'a) -> 'a -> Constr.constr -> 'a

deprecated Alias for [Constr.fold]

val map_constr : 
  (Constr.constr -> Constr.constr) ->
  Constr.constr ->
  Constr.constr

deprecated Alias for [Constr.map]

val map_constr_with_binders : 
  ('a -> 'a) ->
  ('a -> Constr.constr -> Constr.constr) ->
  'a ->
  Constr.constr ->
  Constr.constr

deprecated Alias for [Constr.map_with_binders]

val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses

deprecated Alias for [Constr.map_puniverses]

val univ_of_sort : Sorts.t -> Univ.Universe.t

deprecated Alias for [Sorts.univ_of_sort]

val sort_of_univ : Univ.Universe.t -> Sorts.t

deprecated Alias for [Sorts.sort_of_univ]

val iter_constr : (Constr.constr -> unit) -> Constr.constr -> unit

deprecated Alias for [Constr.iter]

val iter_constr_with_binders : 
  ('a -> 'a) ->
  ('a -> Constr.constr -> unit) ->
  'a ->
  Constr.constr ->
  unit

deprecated Alias for [Constr.iter_with_binders]

val compare_constr : 
  (int -> Constr.constr -> Constr.constr -> bool) ->
  int ->
  Constr.constr ->
  Constr.constr ->
  bool

deprecated Alias for [Constr.compare_head]

type constr = Constr.constr

deprecated Alias for Constr.t

type types = Constr.types

deprecated Alias for Constr.types

type contents = Sorts.contents =

| Pos
| Null

deprecated Alias for Sorts.contents

type sorts = Sorts.t =

| Prop of Sorts.contents
| Type of Univ.Universe.t

deprecated Alias for Sorts.t

type sorts_family = Sorts.family =

| InProp
| InSet
| InType

deprecated Alias for Sorts.family

type !'a puniverses = 'a Univ.puniverses

deprecated Alias for Constr.puniverses

type pconstant = Constr.pconstant

deprecated Alias for Constr.pconstant

type pinductive = Constr.pinductive

deprecated Alias for Constr.pinductive

type pconstructor = Constr.pconstructor

deprecated Alias for Constr.pconstructor

type existential_key = Evar.t

deprecated Alias for Evar.t

type existential = Constr.existential

deprecated Alias for Constr.existential

type metavariable = Constr.metavariable

deprecated Alias for Constr.metavariable

type case_style = Constr.case_style =

| LetStyle
| IfStyle
| LetPatternStyle
| MatchStyle
| RegularStyle

deprecated Alias for Constr.case_style

type case_printing = Constr.case_printing = {

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

}

deprecated Alias for Constr.case_printing

type case_info = Constr.case_info = {

ci_ind : Names.inductive;
ci_npar : int;
ci_cstr_ndecls : int array;
ci_cstr_nargs : int array;
ci_pp_info : Constr.case_printing;

}

deprecated Alias for Constr.case_info

type cast_kind = Constr.cast_kind =

| VMcast
| NATIVEcast
| DEFAULTcast
| REVERTcast

deprecated Alias for Constr.cast_kind

type rec_declaration = Constr.rec_declaration

deprecated Alias for Constr.rec_declaration

type fixpoint = Constr.fixpoint

deprecated Alias for Constr.fixpoint

type cofixpoint = Constr.cofixpoint

deprecated Alias for Constr.cofixpoint

type !'constr pexistential = 'constr Constr.pexistential

deprecated Alias for Constr.pexistential

type (!'constr, !'types) prec_declaration =
  ('constr, 'types) Constr.prec_declaration

deprecated Alias for Constr.prec_declaration

type (!'constr, !'types) pfixpoint = ('constr, 'types) Constr.pfixpoint

deprecated Alias for Constr.pfixpoint

type (!'constr, !'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint

deprecated Alias for Constr.pcofixpoint

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

| Rel of int
| Var of Names.Id.t
| Meta of Constr.metavariable
| Evar of 'constr Constr.pexistential
| Sort of 'sort
| Cast of 'constr * 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 Constr.case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) Constr.pfixpoint
| CoFix of ('constr, 'types) Constr.pcofixpoint
| Proj of Names.Projection.t * 'constr

deprecated Alias for Constr.kind_of_term

type values = Vmvalues.values

deprecated Alias for Vmvalues.values

val hash_constr : Constr.constr -> int

deprecated Alias for Constr.hash

val hcons_sorts : Sorts.t -> Sorts.t

deprecated Alias for [Sorts.hcons]

val hcons_constr : Constr.constr -> Constr.constr

deprecated Alias for [Constr.hcons]

val hcons_types : Constr.types -> Constr.types

deprecated Alias for [Constr.hcons]

package coq