package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz

sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.tactics/Indrec/index.html

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

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

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.

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