style: avoid using @ symbol

Using the `@` symbol is a bit old-fashioned. Co-authored-by: François G. Dorais <[email protected]>
leanprover-community · Oct 15, 2024 · df77496 · df77496
1 parent 20de1c3
commit df77496
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
@@ -21,7 +21,7 @@ namespace List
 
 /-! ### head and tail -/
 
-theorem head_cons_tail : ∀ l h, @head α l h :: l.tail = l
+theorem head_cons_tail : ∀ (l : List α) (hne : l ≠ []), l.head hne :: l.tail = l
   | _::_, _ => rfl
 
 theorem singleton_head_eq_self (l : List α) (hne : l ≠ []) (htl : l.tail = []) :