/Prelude-v23.0.0/Optional/last.dhall

Copy path to clipboard

Returns the last non-empty Optional value in a List

Examples

last Natural [ None Natural, Some 1, Some 2 ] ≡ Some 2
last Natural [ None Natural, None Natural ] ≡ None Natural
last Natural ([] : List (Optional Natural)) ≡ None Natural

Source

--| Returns the last non-empty `Optional` value in a `List`
let last
: ∀(a : Type) → List (Optional a) → Optional a
= λ(a : Type) →
λ(xs : List (Optional a)) →
List/fold
(Optional a)
xs
(Optional a)
( λ(l : Optional a) →
λ(r : Optional a) →
merge { Some = λ(x : a) → Some x, None = l } r
)
(None a)

let example0 = assert : last Natural [ None Natural, Some 1, Some 2 ] ≡ Some 2

let example1 =
assert : last Natural [ None Natural, None Natural ] ≡ None Natural

let example2 =
assert : last Natural ([] : List (Optional Natural)) ≡ None Natural

in last