Commit 2025-03-12 13:47 121c5ee4

View on Github →

chore(Data/List): address most porting notes (#22830) Lots of the porting notes are about "this definition changed in Lean 4", which I think we can just directly discard. A few notes about changed proofs remain.

Estimated changes

Modified Mathlib/Data/List/AList.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/List/Defs.lean

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Data/List/FinRange.lean

Modified Mathlib/Data/List/Lemmas.lean

Modified Mathlib/Data/List/Map2.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/List/Sort.lean

modified theorem List.sorted_singleton

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/List/TakeDrop.lean