package coq
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 =
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 : case_printing;
}
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 =
| 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 * '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 * '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
val destRel : constr -> int
val destMeta : constr -> metavariable
val destVar : constr -> Names.Id.t
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 destConst : constr -> Names.constant puniverses
val destEvar : constr -> existential
val destInd : constr -> Names.inductive puniverses
val destConstruct : constr -> Names.constructor puniverses
val destProj : constr -> Names.projection * constr
val destCoFix : constr -> cofixpoint
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 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 it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
val it_mkProd_or_LetIn : types -> Context.Rel.t -> 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
type arity = Context.Rel.t * sorts
val isArity : types -> bool
type (!'constr, !'types) kind_of_type =
| SortType of sorts
| 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 : types -> (constr, types) kind_of_type
val set_sort : sorts
val prop_sort : sorts
val type1_sort : sorts
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 mkProp : types
val mkSet : types
val mkType : Univ.universe -> types
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 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 mkIndU : Names.inductive puniverses -> constr
val mkConstructU : Names.constructor puniverses -> constr
val mkConstructUi : (pinductive * int) -> constr
val mkCoFix : cofixpoint -> constr
val eq_constr_univs : constr UGraph.check_function
val leq_constr_univs : constr UGraph.check_function
val kind_of_term :
constr ->
(constr, types, Sorts.t, Univ.Instance.t) kind_of_term
val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
val univ_of_sort : sorts -> Univ.universe
val sort_of_univ : Univ.universe -> sorts
val hash_constr : constr -> int
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>