package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type contents = Sorts.contents =
  1. | Pos
  2. | Null
type sorts = Sorts.t =
  1. | Prop of contents
  2. | Type of Univ.universe
type sorts_family = Sorts.family =
  1. | InProp
  2. | InSet
  3. | InType
type !'a puniverses = 'a Univ.puniverses
type pconstant = Names.constant puniverses
type pinductive = Names.inductive puniverses
type pconstructor = Names.constructor puniverses
type constr = Constr.constr
type types = Constr.types
type existential_key = Constr.existential_key
type existential = Constr.existential
type metavariable = Constr.metavariable
type case_style = Constr.case_style =
  1. | LetStyle
  2. | IfStyle
  3. | LetPatternStyle
  4. | MatchStyle
  5. | RegularStyle
type case_printing = Constr.case_printing = {
  1. ind_tags : bool list;
  2. cstr_tags : bool list array;
  3. style : case_style;
}
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 : case_printing;
}
type cast_kind = Constr.cast_kind =
  1. | VMcast
  2. | NATIVEcast
  3. | DEFAULTcast
  4. | REVERTcast
type rec_declaration = Constr.rec_declaration
type fixpoint = Constr.fixpoint
type cofixpoint = Constr.cofixpoint
type !'constr pexistential = 'constr Constr.pexistential
type (!'constr, !'types) prec_declaration = ('constr, 'types) Constr.prec_declaration
type (!'constr, !'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
type (!'constr, !'types) pcofixpoint = ('constr, 'types) 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 metavariable
  4. | Evar of 'constr pexistential
  5. | Sort of 'sort
  6. | Cast of '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 * 'univs
  12. | Ind of Names.inductive * 'univs
  13. | Construct of Names.constructor * 'univs
  14. | Case of case_info * 'constr * 'constr * 'constr array
  15. | Fix of ('constr, 'types) pfixpoint
  16. | CoFix of ('constr, 'types) pcofixpoint
  17. | Proj of Names.projection * 'constr
type values = Constr.values
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 -> bool
exception DestKO
val destRel : constr -> int
val destMeta : constr -> metavariable
val destVar : constr -> Names.Id.t
val destSort : constr -> sorts
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 destApplication : constr -> constr * constr array
val decompose_app : constr -> constr * constr list
val decompose_appvect : constr -> constr * constr array
val destConst : constr -> Names.constant puniverses
val destEvar : constr -> existential
val destConstruct : constr -> Names.constructor puniverses
val destCase : constr -> case_info * constr * constr * constr array
val destProj : constr -> Names.projection * constr
val destFix : constr -> fixpoint
val destCoFix : constr -> cofixpoint
val mkArrow : types -> types -> constr
val mkNamedLambda : Names.Id.t -> types -> constr -> constr
val mkNamedLetIn : Names.Id.t -> constr -> types -> constr -> constr
val mkNamedProd : Names.Id.t -> types -> types -> types
val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types
val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types
val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr
val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr
val applist : (constr * constr list) -> constr
val applistc : constr -> constr list -> constr
val appvect : (constr * constr array) -> constr
val appvectc : constr -> constr array -> constr
val prodn : int -> (Names.Name.t * constr) list -> constr -> constr
val compose_prod : (Names.Name.t * constr) list -> constr -> constr
val lamn : int -> (Names.Name.t * constr) list -> constr -> constr
val compose_lam : (Names.Name.t * constr) list -> constr -> constr
val to_lambda : int -> constr -> constr
val to_prod : int -> constr -> constr
val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
val lambda_applist : constr -> constr list -> constr
val lambda_appvect : constr -> constr array -> constr
val lambda_applist_assum : int -> constr -> constr list -> constr
val lambda_appvect_assum : int -> constr -> constr array -> constr
val prod_appvect : types -> constr array -> types
val prod_applist : types -> constr list -> types
val prod_appvect_assum : int -> types -> constr array -> types
val prod_applist_assum : int -> types -> constr list -> types
val decompose_prod : constr -> (Names.Name.t * constr) list * constr
val decompose_lam : constr -> (Names.Name.t * constr) list * constr
val decompose_prod_n : int -> constr -> (Names.Name.t * constr) list * constr
val decompose_lam_n : int -> constr -> (Names.Name.t * constr) list * constr
val decompose_prod_assum : types -> Context.Rel.t * types
val decompose_lam_assum : constr -> Context.Rel.t * constr
val decompose_prod_n_assum : int -> types -> Context.Rel.t * types
val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr
val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr
val prod_assum : types -> Context.Rel.t
val lam_assum : constr -> Context.Rel.t
val prod_n_assum : int -> types -> Context.Rel.t
val lam_n_assum : int -> constr -> Context.Rel.t
val strip_prod : types -> types
val strip_lam : constr -> constr
val strip_prod_n : int -> types -> types
val strip_lam_n : int -> constr -> constr
val strip_prod_assum : types -> types
val strip_lam_assum : constr -> constr
type arity = Context.Rel.t * sorts
val mkArity : arity -> types
val destArity : types -> arity
val isArity : types -> bool
type (!'constr, !'types) kind_of_type =
  1. | SortType of sorts
  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 kind_of_type : types -> (constr, types) kind_of_type
val set_sort : sorts
val prop_sort : sorts
val type1_sort : sorts
val sorts_ord : sorts -> sorts -> int
val is_prop_sort : sorts -> bool
val family_of_sort : sorts -> sorts_family
val mkRel : int -> constr
val mkVar : Names.Id.t -> constr
val mkMeta : metavariable -> constr
val mkEvar : existential -> constr
val mkSort : sorts -> types
val mkProp : types
val mkSet : types
val mkType : Univ.universe -> types
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 mkConst : Names.constant -> constr
val mkProj : (Names.projection * constr) -> constr
val mkInd : Names.inductive -> constr
val mkConstruct : Names.constructor -> constr
val mkConstU : Names.constant puniverses -> constr
val mkConstructU : Names.constructor puniverses -> constr
val mkConstructUi : (pinductive * int) -> constr
val mkCase : (case_info * constr * constr * constr array) -> constr
val mkFix : fixpoint -> constr
val mkCoFix : cofixpoint -> constr
val eq_constr : constr -> constr -> bool
val eq_constr_univs : constr UGraph.check_function
val leq_constr_univs : constr UGraph.check_function
val eq_constr_nounivs : constr -> constr -> bool
val compare : constr -> constr -> int
val constr_ord : constr -> constr -> int
val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
val map_constr : (constr -> constr) -> constr -> constr
val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
val univ_of_sort : sorts -> Univ.universe
val sort_of_univ : Univ.universe -> sorts
val iter_constr : (constr -> unit) -> constr -> unit
val iter_constr_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
val hash_constr : constr -> int
val hcons_sorts : sorts -> sorts
val hcons_constr : constr -> constr
val hcons_types : types -> types
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