Commit 2025-02-21 13:51 82253b6d

View on Github →

chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn (#22156) By the naming convention, these should be named foo_sumInl etc.

Estimated changes

Modified Mathlib/Computability/Halting.lean

Modified Mathlib/Computability/Partrec.lean

added theorem Computable.sumCasesOn

added theorem Computable.sumInl

added theorem Computable.sumInr

deleted theorem Computable.sum_casesOn

deleted theorem Computable.sum_inl

deleted theorem Computable.sum_inr

added theorem Partrec.optionCasesOn_right

deleted theorem Partrec.option_casesOn_right

added theorem Partrec.sumCasesOn_left

added theorem Partrec.sumCasesOn_right

deleted theorem Partrec.sum_casesOn_left

deleted theorem Partrec.sum_casesOn_right

Modified Mathlib/Computability/Primrec.lean

added theorem Primrec.sumCasesOn

added theorem Primrec.sumInl

added theorem Primrec.sumInr

deleted theorem Primrec.sum_casesOn

deleted theorem Primrec.sum_inl

deleted theorem Primrec.sum_inr

Modified Mathlib/Computability/Reduce.lean