Commit 2023-01-20 17:48 19e2b8d2

View on Github →

fix: make List.rec and Nat.rec computable (#1720) This works around https://github.com/leanprover/lean4/issues/2049. By manually adding compiler support for these recursors, we make a large number of porting notes redundant.

Estimated changes

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

added def FreeMonoid.recOn

Modified Mathlib/Data/Fin/Basic.lean

added def Fin.cases

added def Fin.induction

added def Fin.inductionOn

Modified Mathlib/Data/Fin/Tuple/Basic.lean

added def Fin.cons

Modified Mathlib/Data/Finset/Pi.lean

added def Finset.pi

Modified Mathlib/Data/Fintype/Pi.lean

added def Fintype.piFinset

Modified Mathlib/Data/Fintype/Vector.lean

Modified Mathlib/Data/List/Defs.lean

added def List._sizeOf_instC.{u}

added theorem List._sizeOfinst_eq_sizeOfinstC

added def List.recC.{u_1,

added theorem List.rec_eq_recC

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Multiset/Pi.lean

Modified Mathlib/Data/Multiset/Sections.lean

added def Multiset.Sections

Modified Mathlib/Data/PNat/Basic.lean

Modified Mathlib/Data/Vector/Basic.lean

added def Vector.inductionOn

added def Vector.inductionOn₂

added def Vector.inductionOn₃

Modified Mathlib/Init/Data/Nat/Basic.lean

added def Nat.recC.{u}

added theorem Nat.rec_eq_recC