package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception DestKO
  • deprecated Alias for [Constr.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]
  • 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]
  • deprecated Alias for [Constr.destCast]
  • deprecated Alias for [Constr.destProd]
  • deprecated Alias for [Constr.destLambda]
  • 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]
  • deprecated Alias for [Constr.destConst]
  • deprecated Alias for [Constr.destEvar]
  • deprecated Alias for [Constr.destInd]
  • deprecated Alias for [Constr.destConstruct]
  • deprecated Alias for [Constr.destCase]
  • deprecated Alias for [Constr.destProj]
  • deprecated Alias for [Constr.destFix]
val destCoFix : Constr.constr -> Constr.cofixpoint
  • deprecated Alias for [Constr.destCoFix]
val mkNamedLambda : Names.Id.t -> Constr.types -> Constr.constr -> Constr.constr
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 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 =
  1. | SortType of Sorts.t
  2. | CastType of 'types * 'types
  3. | ProdType of Names.Name.t * 'types * 'types
  4. | LetInType of Names.Name.t * 'constr * 'types * 'types
  5. | AtomicType of 'constr * 'constr array
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
  • deprecated Alias for Constr.mkMeta
  • 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
  • deprecated Alias for Constr.mkType
  • deprecated Alias for Constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr
val mkApp : (Constr.constr * Constr.constr array) -> Constr.constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr
val mkConstruct : Names.constructor -> Constr.constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr
val mkConstructUi : (Constr.pinductive * int) -> Constr.constr
  • deprecated Alias for Constr
  • deprecated Alias for Constr.mkCase
  • deprecated Alias for Constr.mkFix
  • 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
  • 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]
  • 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 =
  1. | Pos
  2. | Null
  • deprecated Alias for Sorts.contents
type sorts = Sorts.t =
  1. | Prop of Sorts.contents
  2. | Type of Univ.Universe.t
  • deprecated Alias for Sorts.t
type sorts_family = Sorts.family =
  1. | InProp
  2. | InSet
  3. | 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 =
  1. | LetStyle
  2. | IfStyle
  3. | LetPatternStyle
  4. | MatchStyle
  5. | RegularStyle
  • deprecated Alias for Constr.case_style
type case_printing = Constr.case_printing = {
  1. ind_tags : bool list;
  2. cstr_tags : bool list array;
  3. style : Constr.case_style;
}
  • deprecated Alias for Constr.case_printing
type case_info = Constr.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_pp_info : Constr.case_printing;
}
  • deprecated Alias for Constr.case_info
type cast_kind = Constr.cast_kind =
  1. | VMcast
  2. | NATIVEcast
  3. | DEFAULTcast
  4. | 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 =
  1. | Rel of int
  2. | Var of Names.Id.t
  3. | Meta of Constr.metavariable
  4. | Evar of 'constr Constr.pexistential
  5. | Sort of 'sort
  6. | Cast of 'constr * Constr.cast_kind * 'types
  7. | Prod of Names.Name.t * 'types * 'types
  8. | Lambda of Names.Name.t * 'types * 'constr
  9. | LetIn of Names.Name.t * '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 Constr.case_info * 'constr * 'constr * 'constr array
  15. | Fix of ('constr, 'types) Constr.pfixpoint
  16. | CoFix of ('constr, 'types) Constr.pcofixpoint
  17. | 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]
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct