package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad
doc/rocq-runtime.tactics/Elimschemes/index.html
Module ElimschemesSource
Declare an inductive should be eliminated dependently even though it's in Prop
Check if an inductive should be eliminated dependently even though it's in Prop
Source
val pseudo_sort_quality_for_elim :
Names.inductive ->
Declarations.one_inductive_body ->
Sorts.Quality.tLegacy API, returns the quality of the inductive except if it's prop_but_default_dependent_elim in which case we return Type instead.
Returns false on inductives which cannot be eliminated dependently or are in Prop without being declared prop_but_default_dependent_elim.
Source
val elim_scheme :
dep:bool ->
to_kind:UnivGen.QualityOrSet.t ->
Ind_tables.individual Ind_tables.scheme_kindInduction/recursion schemes
Case analysis schemes
Recursor names utilities
Source
val lookup_eliminator :
Environ.env ->
Names.inductive ->
UnivGen.QualityOrSet.t ->
Names.GlobRef.t