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=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759

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