Option of a type #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file develops the basic theory of option types.
α 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
with_bot αwhich uses
noneas an element smaller than all others.
- It can be used to define failsafe partial functions, which return
some the_result_we_expectif we can find
noneif there is no meaningful result. This forces any subsequent use of the partial function to explicitly deal with the exceptions that make it return
optionis a monad. We love monads.
part is an alternative to
option that can be seen as the type of
along with a term
a : α if the value is
Implementation notes #
option is currently defined in core Lean, but this will change in Lean 4.
option.map f is injective if
f is injective.
option.map as a function between functions is injective.
Given an element of
a : option α, a default element
b : β and a function
α → β, apply this
a if it comes from
α, and return
- (option.some a).cases_on' n s = s a
- option.none.cases_on' n s = n
some a with
a : α if
α is nonempty, and otherwise
- option.choice α = dite (nonempty α) (λ (h : nonempty α), option.some h.some) (λ (h : ¬nonempty α), option.none)