ElimschemesSourceDeclare 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
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.
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
val lookup_eliminator :
Environ.env ->
Names.inductive ->
UnivGen.QualityOrSet.t ->
Names.GlobRef.t