Indrec (p.rocq-runtime.9.2.0.doc.rocq-runtime.tactics.Indrec)

Sourcetype dep_flag = bool

Eliminations

Sourcetype recursion_scheme_error =

| NotMutualInScheme of Names.inductive * Names.inductive
| DuplicateInductiveBlock of Names.inductive

Errors related to recursors building

Sourceexception RecursionSchemeError of Environ.env * recursion_scheme_error

val build_case_analysis_scheme : 
  Environ.env ->
  Evd.evar_map ->
  Names.inductive Evd.puniverses ->
  dep_flag ->
  EConstr.ESorts.t ->
  Evd.evar_map * EConstr.constr * EConstr.constr

Source

val build_induction_scheme : 
  Environ.env ->
  Evd.evar_map ->
  Names.inductive Evd.puniverses ->
  dep_flag ->
  EConstr.ESorts.t ->
  Evd.evar_map * EConstr.constr

Builds a recursive induction scheme (Peano-induction style) in the given sort.

Source

val build_mutual_induction_scheme : 
  Environ.env ->
  Evd.evar_map ->
  ?force_mutual:bool ->
  (Names.inductive * dep_flag * EConstr.ESorts.t) list ->
  Evd.einstance ->
  Evd.evar_map * EConstr.constr list

Builds mutual (recursive) induction schemes