From c9c85c7d83a929e4686d17958350be43d37df75b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 25 Feb 2025 11:53:37 +1100 Subject: [PATCH] chore: List.leftpad typo (#7219) --- src/Init/Data/List/Nat/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean index ac02383dc828..b96cdaa4f7c8 100644 --- a/src/Init/Data/List/Nat/Basic.lean +++ b/src/Init/Data/List/Nat/Basic.lean @@ -95,12 +95,12 @@ theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) : to the larger of `n` and `l.length` -/ -- We don't mark this as a `@[simp]` lemma since we allow `simp` to unfold `leftpad`, -- so the left hand side simplifies directly to `n - l.length + l.length`. -theorem length_lengthpad (n : Nat) (a : α) (l : List α) : +theorem length_leftpad (n : Nat) (a : α) (l : List α) : (leftpad n a l).length = max n l.length := by simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max] -@[deprecated length_lengthpad (since := "2025-02-24")] -abbrev leftpad_length := @length_lengthpad +@[deprecated length_leftpad (since := "2025-02-24")] +abbrev leftpad_length := @length_leftpad theorem length_rightpad (n : Nat) (a : α) (l : List α) : (rightpad n a l).length = max n l.length := by