Option of a type #
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.
Implementation notes #
option is currently defined in core Lean, but this will change in Lean 4.