dhall-1.21.0: dhall-lang/Prelude/Optional/build

{-
`build` is the inverse of `fold`

Examples:

```
./build
Natural
(   λ(optional : Type)
→   λ(some : Natural → optional)
→   λ(none : optional)
→   some 1
)
= Some 1

./build
Natural
(   λ(optional : Type)
→   λ(some : Natural → optional)
→   λ(none : optional)
→   none
)
= None Natural
```
-}
    let build
        :   ∀(a : Type)
          → (   ∀(optional : Type)
              → ∀(some : a → optional)
              → ∀(none : optional)
              → optional
            )
          → Optional a
        = Optional/build

in  build