/Prelude-v22.0.0/Optional/default.dhall

Copy path to clipboard

Unpack an Optional, returning the default when it's None.

Examples

default Bool False (None Bool) ≡ False
default Bool False (Some True) ≡ True

Source

--| 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) →
merge { Some = λ(x : a) → x, None = default } o

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

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

in default