Skip to content

Commit

Permalink
chore: List.leftpad typo (#7219)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Feb 25, 2025
1 parent d615e61 commit c9c85c7
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/Init/Data/List/Nat/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit c9c85c7

Please sign in to comment.