dhall-1.24.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