dhall-1.27.0: dhall-lang/Prelude/Optional/default

{-
Unpack an `Optional`, returning the default when it's `None`.
-}
let default
    : ∀(a : Type) → a → Optional a → a
    =   λ(a : Type)
      → λ(default : a)
      → λ(o : Optional a)
      → Optional/fold a o a (λ(x : a) → x) default

let example0 = assert : default Bool False (None Bool) ≡ False

let example1 = assert : default Bool False (Some True) ≡ True

in  default