package coq

  1. Overview
  2. Docs
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.