This PR optimizes a few simple List functions by using pattern matching instead of calling other functions.
It also fixes the doc of List.tail and adds examples.
data.List.unsnoc : [a] -> Optional ([a], a)
data.List.unsnoc = cases
xs :+ x -> Some (xs, x)
[] -> None
data.List.last : [a] -> Optional a
data.List.last = cases
_ :+ x -> Some x
[] -> None
data.List.uncons : [a] -> Optional (a, [a])
data.List.uncons = cases
x +: xs -> Some (x, xs)
[] -> None
data.List.tail : [a] -> Optional [a]
data.List.tail = cases
_ +: xs -> Some xs
[] -> None
Old Code
data.List.unsnoc : [a] -> Optional ([a], a)
data.List.unsnoc as =
i = List.size (List.drop 1 as)
match List.at i as with
None -> None
Some a -> Some (List.take i as, a)
data.List.last : [a] -> Optional a
data.List.last xs =
use Nat -
List.at (List.size xs - 1) xs
data.List.uncons : [a] -> Optional (a, [a])
data.List.uncons as = match List.at 0 as with
None -> None
Some a -> Some (a, List.drop 1 as)
data.List.tail : [a] -> Optional [a]
data.List.tail xs = Optional.map at2 (List.uncons xs)
This PR optimizes a few simple
List
functions by using pattern matching instead of calling other functions. It also fixes the doc ofList.tail
and adds examples.Here is the PR branch.
New Code
Old Code