diff options
| author | Andreas Grois <andi@grois.info> | 2024-09-18 19:42:46 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-09-18 19:42:46 +0200 |
| commit | 2c1f2362c69ab20b10b61bdbebf8e5121eca38b1 (patch) | |
| tree | b31f7e8fff82630d33319b231cf2868d5922cb30 /Common/List.lean | |
| parent | 6554499717d70d5656a3b38a20dc60850674a873 (diff) | |
Continue Day11/Parsing
Diffstat (limited to 'Common/List.lean')
| -rw-r--r-- | Common/List.lean | 5 |
1 files changed, 5 insertions, 0 deletions
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⟩ |