dhall-1.24.0: dhall-lang/Prelude/Optional/last

{-
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
```
-}
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) → Some x) l
        )
        (None a)

in  last