last

{-
Returns the last non-empty `Optional` value in a `List`

Examples:

```
./last
Natural
[ [   ] : Optional Natural
, [ 1 ] : Optional Natural
, [ 2 ] : Optional Natural
]
= [ 2 ] : Optional Natural

./last
Natural
[ [] : Optional Natural, [] : Optional Natural ]
= [] : Optional Natural

./last Natural ([] : List (Optional Natural))
= [] : Optional Natural
```
-}
    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)
              → Optional/fold a r (Optional a) (λ(x : a) → [ x ] : Optional a) l
            )
            ([] : Optional a)

in  last