Option α 是值的类型，对于某些 v:α 为 some v，或 none。
在函数式编程中，此类型的使用方式与可空类型类似：none 表示不存在值。
此外，从 α 到 β 的部分函数可以由类型 α → Option β 表示，其中当函数对于某些输入未定义时，结果为 none。
从计算角度来看，这些部分函数代表了失败或错误的可能性，它们对应于可以提前终止但不会抛出信息性异常的程序。
Option 也可以被认为类似于最多包含一个元素的列表。
从这个角度来看，迭代 Option 包括仅当值存在时才执行操作。
Option API 经常使用这个视角。
函数 Std.HashMap.get? 在 HashMap α β 内查找指定的键 a : α：
Std.HashMap.get?.{u, v} {α : Type u} {β : Type v}
[BEq α] [Hashable α]
(m : HashMap α β) (a : α) :
Option β
由于无法提前知道该键是否确实在映射中，因此返回类型为 Option β，其中 none 表示该键不在映射中，some b 表示找到该键，b 是检索到的值。
xs[i] 语法用于在有可用证据证明 i 是 xs 中的有效索引时对集合进行索引，它有一个变体 xs[i]?，它根据给定索引是否有效返回一个可选值。
如果 m:HashMap α β 和 a:α，则 m[a]? 相当于 HashMap.get? m a。
在许多编程语言中，记住检查空值非常重要。
使用 Option 时，类型系统要求在正确的位置进行这些检查：Option α 和 α 不是同一类型，从一种类型转换为另一种类型需要处理 none 的情况。
这可以通过 Option.getD 等帮助程序或模式匹配来完成。
def postalCodes : Std.HashMap Nat String :=
Std.HashMap.emptyWithCapacity 1 |>.insert 12345 "Schenectady"
#eval postalCodes[12346]?.getD "not found"
#eval
match postalCodes[12346]? with
| none => "not found"
| some city => city
#eval
if let some city := postalCodes[12345]? then
city
else
"not found"
Optional values, which are either some around a value from the underlying type or none.
Option can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
Option.none.{u} {α : Type u} : Option α
No value.
Option.some.{u} {α : Type u} (val : α) : Option α
Some value of type α.
有一个从 α 到 Option α 的 强制 将值包装在 some 中。
这允许 Option 的使用方式与其他语言中的可空类型类似，其中缺少的值由 none 指示，而存在的值没有特别标记。
Option.getDM.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (x : Option α) (y : m α) : m αOption.getDM.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (x : Option α) (y : m α) : m α
Gets the value in an option, monadically computing a default value on none.
This is the monadic analogue of Option.getD.
A case analysis function for Option.
Given a value for none and a function to apply to the contents of some, Option.elim checks
which constructor a given Option consists of, and uses the appropriate argument.
Option.elim is an elimination principle for Option. In particular, it is a non-dependent version
of Option.recOn. It can also be seen as a combination of Option.map and Option.getD.
Examples:
(some "hello").elim 0 String.length = 5
none.elim 0 String.length = 0
Option.elimM.{u_1, u_2} {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] (x : m (Option α)) (y : m β) (z : α → m β) : m βOption.elimM.{u_1, u_2} {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] (x : m (Option α)) (y : m β) (z : α → m β) : m β
A monadic case analysis function for Option.
Given a fallback computation for none and a monadic operation to apply to the contents of some,
Option.elimM checks which constructor a given Option consists of, and uses the appropriate
argument.
Option.elimM can also be seen as a combination of Option.mapM and Option.getDM. It is a
monadic analogue of Option.elim.
Applies a function to a two optional values if both are present. Otherwise, if one value is present, it is returned and the function is not used.
The value is some (fn a b) if the inputs are some a and some b. Otherwise, the behavior is
equivalent to Option.orElse: if only one input is some x, then the value is some x, and if
both are none, then the value is none.
Examples:
Option.merge (· + ·) none (some 3) = some 3
Option.merge (· + ·) (some 2) (some 3) = some 5
Option.merge (· + ·) (some 2) none = some 2
Option.merge (· + ·) none none = none
可选值的排序通常使用 DecidableEq (Option α)、LT (Option α)、Min (Option α) 和 Max (Option α) 实例。
The minimum of two optional values, with none treated as the least element. This function is
usually accessed through the Min (Option α) instance, rather than directly.
Prior to nightly-2025-02-27, none was treated as the greatest element, so
min none (some x) = min (some x) none = some x.
Examples:
Option.min (some 2) (some 5) = some 2
Option.min (some 5) (some 2) = some 2
Option.min (some 2) none = none
Option.min none (some 5) = none
Option.min none none = none
The maximum of two optional values.
This function is usually accessed through the Max (Option α) instance, rather than directly.
Examples:
Option.max (some 2) (some 5) = some 5
Option.max (some 5) (some 2) = some 5
Option.max (some 2) none = some 2
Option.max none (some 5) = some 5
Option.max none none = none
Lifts an ordering relation to Option, such that none is the least element.
It can be understood as adding a distinguished least element, represented by none, to both α and
β.
This definition is part of the implementation of the LT (Option α) instance. However, because it
can be used with heterogeneous relations, it is sometimes useful on its own.
Examples:
Formats an optional value, with no expectation that the Lean parser should be able to parse the result.
This function is usually accessed through the ToFormat (Option α) instance.
Option 可以被认为是描述可能无法返回值的计算。
Monad Option 实例以及 Alternative Option 均基于这种理解。
返回 none 也可以被认为是抛出一个不包含任何有趣信息的异常，该异常在 MonadExcept Unit Option 实例中捕获。
Returns none if a value doesn't satisfy a Boolean predicate, or the value itself otherwise.
From the perspective of Option as computations that might fail, this function is a run-time
assertion operator in the Option monad.
Examples:
Option.guard (· > 2) 1 = none
Option.guard (· > 2) 5 = some 5
Sequencing of Option computations.
From the perspective of Option as computations that might fail, this function sequences
potentially-failing computations, failing if either fails. From the perspective of Option as a
collection with at most one element, the function is applied to the element if present, and the
final result is empty if either the initial or the resulting collections are empty.
This function is often accessed via the >>= operator from the Bind (Option α) instance, or
implicitly via do-notation, but it is also idiomatic to call it using generalized field
notation.
Examples:
Option.bindM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Pure m] (f : α → m (Option β)) : Option α → m (Option β)Option.bindM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Pure m] (f : α → m (Option β)) : Option α → m (Option β)
Runs the monadic action f on o's value, if any, and returns the result, or none if there is
no value.
From the perspective of Option as a collection with at most one element, the monadic the function
is applied to the element if present, and the final result is empty if either the initial or the
resulting collections are empty.
Option.sequence.{u, u_1} {m : Type u → Type u_1} [Applicative m] {α : Type u} : Option (m α) → m (Option α)Option.sequence.{u, u_1} {m : Type u → Type u_1} [Applicative m] {α : Type u} : Option (m α) → m (Option α)
Converts an optional monadic computation into a monadic computation of an optional value.
This function only requires m to be an applicative functor.
Example:
#eval show IO (Option String) from
Option.sequence <| some do
IO.println "hello"
return "world"
hello
some "world"
Recover from failing Option computations with a handler function.
This function is usually accessed through the MonadExceptOf Unit Option instance.
Examples:
Option.tryCatch none (fun () => some "handled") = some "handled"
Option.tryCatch (some "succeeded") (fun () => some "handled") = some "succeeded"
Option 可以被认为是最多包含一个值的集合。
从这个角度来看，迭代运算符可以理解为对包含的值（如果存在）执行某些操作，或者如果不存在则不执行任何操作。
Checks whether an optional value either satisfies a Boolean predicate or is none.
Examples:
`(some 33).all (· % 2 == 0) = false
`(some 22).all (· % 2 == 0) = true
`none.all (fun x : Nat => x % 2 == 0) = true
Checks whether an optional value is not none and satisfies a Boolean predicate.
Examples:
`(some 33).any (· % 2 == 0) = false
`(some 22).any (· % 2 == 0) = true
`none.any (fun x : Nat => true) = false
Keeps an optional value only if it satisfies a Boolean predicate.
If Option is thought of as a collection that contains at most one element, then Option.filter is
analogous to List.filter or Array.filter.
Examples:
Option.filterM.{u_1} {m : Type → Type u_1} {α : Type} [Applicative m] (p : α → m Bool) : Option α → m (Option α)Option.filterM.{u_1} {m : Type → Type u_1} {α : Type} [Applicative m] (p : α → m Bool) : Option α → m (Option α)
Keeps an optional value only if it satisfies a monadic Boolean predicate.
If Option is thought of as a collection that contains at most one element, then Option.filterM
is analogous to List.filterM.
Option.forM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} [Pure m] : Option α → (α → m PUnit) → m PUnitOption.forM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} [Pure m] : Option α → (α → m PUnit) → m PUnit
Option.mapA.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] (f : α → m β) : Option α → m (Option β)Option.mapA.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] (f : α → m β) : Option α → m (Option β)
Applies a function in some applicative functor to an optional value, returning none with no
effects if the value is missing.
This is an alias for Option.mapM, which already works for applicative functors.
Option.mapM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] (f : α → m β) : Option α → m (Option β)Option.mapM.{u_1, u_2, u_3} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Applicative m] (f : α → m β) : Option α → m (Option β)
Applies a function in some applicative functor to an optional value, returning none with no
effects if the value is missing.
Runs a monadic function f on an optional value, returning the result. If the optional value is
none, the function is not called and the result is also none.
From the perspective of Option as a container with at most one element, this is analogous to
List.mapM, returning the result of running the monadic function on all elements of the container.
This function only requires m to be an applicative functor. An alias Option.mapA is provided.
“Attaches” a proof that an optional value, if present, is indeed this value, returning a subtype that expresses this fact.
This function is primarily used to allow definitions by well-founded recursion that use iteration
operators (such as Option.map) to prove that an optional value drawn from a parameter is smaller
than the parameter. This allows the well-founded recursion mechanism to prove that the function
terminates.
“Attaches” a proof that some predicate holds for an optional value, if present, returning a subtype that expresses this fact.
This function is primarily used to implement Option.attach, which allows definitions by
well-founded recursion that use iteration operators (such as Option.map) to prove that an optional
value drawn from a parameter is smaller than the parameter. This allows the well-founded recursion
mechanism to prove that the function terminates.
Remove an attached proof that the value in an Option is indeed that value.
This function is usually inserted automatically by Lean, rather than explicitly in code. It is introduced as an intermediate step during the elaboration of definitions by well-founded recursion.
If this function is encountered in a proof state, the right approach is usually the tactic
simp [Option.unattach, -Option.map_subtype].
It is a synonym for Option.map Subtype.val.
Given an optional value and a function that can be applied when the value is some, returns the
result of applying the function if this is possible.
The function f is partial because it is only defined for the values a : α such that
o = some a. This restriction allows the function to use the fact that it can only be called when
o is not none: it can relate its argument to the optional value o. Its runtime behavior is
equivalent to that of Option.bind.
Examples:
def attach (v : Option α) : Option { y : α // v = some y } :=
v.pbind fun x h => some ⟨x, h⟩
#reduce attach (some 3)
some ⟨3, ⋯⟩#reduce attach none
noneOption.pelim.{u_1, u_2} {α : Type u_1} {β : Sort u_2} (o : Option α) (b : β) (f : (a : α) → o = some a → β) : βOption.pelim.{u_1, u_2} {α : Type u_1} {β : Sort u_2} (o : Option α) (b : β) (f : (a : α) → o = some a → β) : β
Given an optional value and a function that can be applied when the value is some, returns the
result of applying the function if this is possible, or a fallback value otherwise.
The function f is partial because it is only defined for the values a : α such that
o = some a. This restriction allows the function to use the fact that it can only be called when
o is not none: it can relate its argument to the optional value o. Its runtime behavior is
equivalent to that of Option.elim.
Examples:
def attach (v : Option α) : Option { y : α // v = some y } :=
v.pelim none fun x h => some ⟨x, h⟩
#reduce attach (some 3)
some ⟨3, ⋯⟩#reduce attach none
noneOption.pmap.{u_1, u_2} {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (o : Option α) : (∀ (a : α), o = some a → p a) → Option βOption.pmap.{u_1, u_2} {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (o : Option α) : (∀ (a : α), o = some a → p a) → Option β
Given a function from the elements of α that satisfy p to β and a proof that an optional value
satisfies p if it's present, applies the function to the value.
Examples:
def attach (v : Option α) : Option { y : α // v = some y } :=
v.pmap (fun a (h : a ∈ v) => ⟨_, h⟩) (fun _ h => h)
#reduce attach (some 3)
some ⟨3, ⋯⟩#reduce attach none
none