diff options
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⟩ |