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

sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

Induction/recursion schemes

val elim_scheme : 
  dep:bool ->
  to_kind:UnivGen.QualityOrSet.t ->
  Ind_tables.individual Ind_tables.scheme_kind

Case analysis schemes

Sourceval case_dep : Ind_tables.individual Ind_tables.scheme_kind

Sourceval case_nodep : Ind_tables.individual Ind_tables.scheme_kind

Sourceval casep_dep : Ind_tables.individual Ind_tables.scheme_kind

Sourceval casep_nodep : Ind_tables.individual Ind_tables.scheme_kind