Skip to content

Commit

Permalink
fix: map_drop had unnecessarily specialized universes (#708)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Mar 22, 2024
1 parent 7b2c022 commit e5306c3
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Std/Data/List/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1115,7 +1115,7 @@ theorem drop_take : ∀ (m n : Nat) (l : List α), drop m (take (m + n) l) = tak
have h : m + 1 + n = m + n + 1 := by rw [Nat.add_assoc, Nat.add_comm 1 n, ← Nat.add_assoc]
simpa [take_cons_succ, h] using drop_take m n l

theorem map_drop {α β : Type u} (f : α → β) :
theorem map_drop (f : α → β) :
∀ (L : List α) (i : Nat), (L.drop i).map f = (L.map f).drop i
| [], i => by simp
| L, 0 => by simp
Expand Down

0 comments on commit e5306c3

Please sign in to comment.