From df7749624a353cf4b99a8bbeaf398c9e02e6e8f6 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Tue, 15 Oct 2024 02:36:25 +0000 Subject: [PATCH] style: avoid using `@` symbol MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Using the `@` symbol is a bit old-fashioned. Co-authored-by: François G. Dorais --- Batteries/Data/List/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean index c14cbd440e..2cf150d3a0 100644 --- 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 = []) :