From 2c1f2362c69ab20b10b61bdbebf8e5121eca38b1 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Wed, 18 Sep 2024 19:42:46 +0200
Subject: Continue Day11/Parsing

---
 Common/List.lean | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Common/List.lean')

diff --git a/Common/List.lean b/Common/List.lean
index 0e8285e..b34f1e2 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -49,3 +49,8 @@ def compare {α : Type} [Ord α] (a b : List α) := match a, b with
 
 instance {α : Type} [Ord α] : Ord (List α) where
   compare := compare
+
+def not_empty_iff_size_gt_zero {list : List α} : list.isEmpty = false ↔ list.length > 0 :=
+  match list with
+  | [] => ⟨nofun, nofun⟩
+  | l :: ls => ⟨λ_ ↦ (List.length_cons l ls).substr (Nat.succ_pos ls.length), λ_ => rfl⟩
-- 
cgit v1.2.3