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

{-
`build` is the inverse of `fold`
-}
let build
    :   ∀(a : Type)
      → (   ∀(optional : Type)
          → ∀(some : a → optional)
          → ∀(none : optional)
          → optional
        )
      → Optional a
    = Optional/build

let example0 =
        assert
      :   build
            Natural
            (   λ(optional : Type)
              → λ(some : Natural → optional)
              → λ(none : optional)
              → some 1
            )
        ≡ Some 1

let example1 =
        assert
      :   build
            Natural
            (   λ(optional : Type)
              → λ(some : Natural → optional)
              → λ(none : optional)
              → none
            )
        ≡ None Natural

in  build