From 35d9307df30c1cbd2ab1103e083c21dd70dbd191 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 6 May 2024 21:14:18 +1000 Subject: [PATCH] chore: move @[simp] attribute on length_eq_zero earlier (#4077) Cleanup. --- src/Init/Data/List/Lemmas.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 702ebddcb2..00070de044 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -54,7 +54,7 @@ theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [ theorem ne_nil_of_length_eq_succ (_ : length l = succ n) : l ≠ [] := fun _ => nomatch l -theorem length_eq_zero : length l = 0 ↔ l = [] := +@[simp] theorem length_eq_zero : length l = 0 ↔ l = [] := ⟨eq_nil_of_length_eq_zero, fun h => h ▸ rfl⟩ /-! ### mem -/ @@ -784,8 +784,6 @@ theorem exists_cons_of_length_succ : ∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t | _::_, _ => ⟨_, _, rfl⟩ -attribute [simp] length_eq_zero -- TODO: suggest to core - @[simp] theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] := Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)