package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Indrec`Source

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

Source

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

package rocq-runtime

Module IndrecSource

Module `Indrec`Source