package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
doc/coq-core.pretyping/Indrec/index.html
Module IndrecSource
Errors related to recursors building
Source
type recursion_scheme_error = | NotAllowedCaseAnalysis of bool * Sorts.t * Constr.pinductive| NotMutualInScheme of Names.inductive * Names.inductive| NotAllowedDependentAnalysis of bool * Names.inductive
Eliminations
Build a case analysis elimination scheme in some sort family
Source
val build_case_analysis_scheme :
Environ.env ->
Evd.evar_map ->
Constr.pinductive ->
dep_flag ->
Sorts.family ->
Evd.evar_map * Constr.tBuild a dependent case elimination predicate unless type is in Prop or is a recursive record with primitive projections.
Source
val build_case_analysis_scheme_default :
Environ.env ->
Evd.evar_map ->
Constr.pinductive ->
Sorts.family ->
Evd.evar_map * Constr.tBuilds a recursive induction scheme (Peano-induction style) in the same sort family as the inductive family; it is dependent if not in Prop or a recursive record with primitive projections.
Source
val build_induction_scheme :
Environ.env ->
Evd.evar_map ->
Constr.pinductive ->
dep_flag ->
Sorts.family ->
Evd.evar_map * Constr.constrBuilds mutual (recursive) induction schemes
Source
val build_mutual_induction_scheme :
Environ.env ->
Evd.evar_map ->
?force_mutual:bool ->
(Constr.pinductive * dep_flag * Sorts.family) list ->
Evd.evar_map * Constr.constr listScheme combinators
weaken_sort_scheme env sigma eq s n c t derives by subtyping from c:t whose conclusion is quantified on Type i at position n of t a scheme quantified on sort s. set asks for s be declared equal to i, otherwise just less or equal to i.
Source
val weaken_sort_scheme :
Environ.env ->
Evd.evar_map ->
bool ->
Sorts.t ->
int ->
Constr.constr ->
Constr.types ->
Evd.evar_map * Constr.types * Constr.constrRecursor names utilities