Elimschemesval declare_prop_but_default_dependent_elim : Names.inductive -> unitDeclare an inductive should be eliminated dependently even though it's in Prop
val is_prop_but_default_dependent_elim : Names.inductive -> boolCheck 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.
val default_case_analysis_dependence : Environ.env -> Names.inductive -> boolReturns 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
val case_dep : Ind_tables.individual Ind_tables.scheme_kindval case_nodep : Ind_tables.individual Ind_tables.scheme_kindval casep_dep : Ind_tables.individual Ind_tables.scheme_kindval casep_nodep : Ind_tables.individual Ind_tables.scheme_kindval scase_dep : Ind_tables.individual Ind_tables.scheme_kindval scase_nodep : Ind_tables.individual Ind_tables.scheme_kindRecursor names utilities
val lookup_eliminator :
Environ.env ->
Names.inductive ->
UnivGen.QualityOrSet.t ->
Names.GlobRef.tval elimination_suffix : UnivGen.QualityOrSet.t -> stringval make_elimination_ident : Names.Id.t -> UnivGen.QualityOrSet.t -> Names.Id.t