2019-04-10 15:01:58 +03:00
|
|
|
use Optional None Some
|
|
|
|
|
|
|
|
lenLit : [a] -> Nat
|
2019-04-10 04:42:43 +03:00
|
|
|
lenLit l = case l of
|
2019-04-06 23:28:50 +03:00
|
|
|
[] -> 0
|
2019-04-10 04:42:43 +03:00
|
|
|
[_] -> 1
|
|
|
|
[_, _] -> 2
|
|
|
|
[_, _, _] -> 3
|
2019-04-09 03:24:41 +03:00
|
|
|
|
2019-04-10 15:01:58 +03:00
|
|
|
lenCons : [a] -> Nat
|
2019-04-10 04:42:43 +03:00
|
|
|
lenCons l = case l of
|
|
|
|
[] -> 0
|
|
|
|
_ +: t -> 1 + lenCons t
|
2019-04-18 01:16:21 +03:00
|
|
|
_ +: (_ +: t) -> 2 + lenCons t
|
2019-04-10 04:42:43 +03:00
|
|
|
|
2019-04-10 15:01:58 +03:00
|
|
|
lenSnoc : [a] -> Nat
|
2019-04-10 04:42:43 +03:00
|
|
|
lenSnoc l = case l of
|
|
|
|
[] -> 0
|
|
|
|
t :+ _ -> 1 + lenSnoc t
|
|
|
|
|
2019-04-18 01:16:21 +03:00
|
|
|
lenConcat1 : [a] -> Nat
|
|
|
|
lenConcat1 l = case l of
|
2019-04-10 04:42:43 +03:00
|
|
|
[] -> 0
|
2019-04-18 01:16:21 +03:00
|
|
|
[_] ++ tail -> 1 + lenConcat1 tail
|
|
|
|
|
|
|
|
lenConcat2 : [a] -> Nat
|
|
|
|
lenConcat2 l = case l of
|
|
|
|
[] -> 0
|
|
|
|
prefix ++ [_] -> 1 + lenConcat2 prefix
|
2019-04-10 04:42:43 +03:00
|
|
|
|
|
|
|
> lenLit [1, 2, 3]
|
2019-04-18 01:16:21 +03:00
|
|
|
> lenCons [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
|
|
|
|
> lenSnoc [1, 2, 3, 4, 5, 6, 7, 8]
|
|
|
|
> lenConcat1 [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11]
|
|
|
|
> lenConcat2 [1, 2, 3, 4, 5]
|
2019-04-10 15:01:58 +03:00
|
|
|
|
|
|
|
head : [a] -> Optional a
|
|
|
|
head l = case l of
|
|
|
|
h +: _ -> Some h
|
|
|
|
_ -> None
|
|
|
|
|
|
|
|
> head []
|
|
|
|
> head [1, 2, 3]
|
|
|
|
|
|
|
|
firstTwo : [a] -> Optional (a, a)
|
|
|
|
firstTwo l = case l of
|
|
|
|
x +: (y +: _) -> Some (x, y)
|
|
|
|
_ -> None
|
|
|
|
|
|
|
|
> firstTwo []
|
|
|
|
> firstTwo [1]
|
|
|
|
> firstTwo [1, 2, 3]
|
|
|
|
|
|
|
|
lastTwo : [a] -> Optional (a, a)
|
|
|
|
lastTwo l = case l of
|
|
|
|
_ :+ x :+ y -> Some (x, y)
|
|
|
|
_ -> None
|
|
|
|
|
|
|
|
> lastTwo []
|
|
|
|
> lastTwo [1]
|
|
|
|
> lastTwo [1, 2, 3]
|
|
|
|
|
|
|
|
middle : [a] -> Optional [a]
|
|
|
|
middle l = case l of
|
|
|
|
[_] ++ m ++ [_] -> Some m
|
|
|
|
_ -> None
|
|
|
|
|
|
|
|
> middle []
|
|
|
|
> middle [1, 2]
|
|
|
|
> middle [1, 2, 3, 4, 5, 6]
|
2019-04-18 01:16:21 +03:00
|
|
|
|
|
|
|
middleNel: [a] -> Optional (a, [a])
|
|
|
|
middleNel l = case l of
|
|
|
|
[_] ++ (h +: t) ++ [_] -> Some (h, t)
|
|
|
|
_ -> None
|
|
|
|
|
|
|
|
> middleNel []
|
|
|
|
> middleNel [1, 2]
|
|
|
|
> middleNel [1, 2, 3, 4, 5, 6]
|