Option of a type #
This file develops the basic theory of option types.
If α
is a type, then Option α
can be understood as the type with one more element than α
.
Option α
has terms some a
, where a : α
, and none
, which is the added element.
This is useful in multiple ways:
- It is the prototype of addition of terms to a type. See for example
WithBot α
which usesnone
as an element smaller than all others. - It can be used to define failsafe partial functions, which return
some the_result_we_expect
if we can findthe_result_we_expect
, andnone
if there is no meaningful result. This forces any subsequent use of the partial function to explicitly deal with the exceptions that make it returnnone
. Option
is a monad. We love monads.
Part
is an alternative to Option
that can be seen as the type of True
/False
values
along with a term a : α
if the value is True
.
Option.map f
is injective if f
is injective.
Option.map
as a function between functions is injective.
Alias of Option.some_orElse
.
Alias of Option.orElse_none
.
Given an element of a : Option α
, a default element b : β
and a function α → β
, apply this
function to a
if it comes from α
, and return b
otherwise.
Instances For
Alias of Option.not_isSome
.
Alias of Option.not_comp_isSome
.
Alias of Option.not_isNone
.
Alias of Option.not_comp_isNone
.
Alias of Option.eq_none_iff_forall_some_ne
.