blob: 6e76f89aa72ab985addcdb1981c2ee8da3830cae (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
structure NonEmptyList (α : Type) where
head : α
tail : List α
namespace NonEmptyList
def toList (l : NonEmptyList α) : List α :=
l.head :: l.tail
def ofList (l : List α) (_ : ¬l.isEmpty) : NonEmptyList α :=
match l with
| head :: tail => {head, tail}
def ofList? (l : List α) : Option $ NonEmptyList α :=
if h : l.isEmpty then
none
else
ofList l h
instance [ToString α] : ToString (NonEmptyList α) where
toString := List.toString ∘ toList
|
