{-
`fold` is the primitive function for consuming `Optional` values

Examples:

```
./fold Natural ([ 2 ] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 2

./fold Natural ([] : Optional Natural) Natural (λ(x : Natural) → x) 0 = 0
```
-}
    let fold
        :   ∀(a : Type)
          → Optional a
          → ∀(optional : Type)
          → ∀(just : a → optional)
          → ∀(nothing : optional)
          → optional
        = Optional/fold

in  fold