Lean 语言参考手册

20.12. 可选值🔗

Option α 是一种值的类型，它可以是某个 some v，其中 v:α；也可以是 none。 在函数式编程中，此类型的使用方式类似于可空类型：none 表示不存在值。 此外，从 α 到 β 的偏函数可以由类型 α → Option β 来表示，当该函数对某些输入未定义时，结果即为 none。 在计算上，这些偏函数表示失败或错误的可能性，并且它们对应于可以提前终止但不抛出包含信息之异常的程序。

Option 也可以被认为类似于最多包含一个元素的列表。 从这个角度来看，遍历 Option 包括仅在存在值时才执行操作。 Option API 经常使用这种视角。

作为可空性的 Option

函数 Std.HashMap.get? 接受键 a : α，并在指定的 HashMap α β 中查找它：

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 时，类型系统会在正确的地方要求进行这些检查：Option α 和 α 不是同一种类型，并且在它们之间进行转换需要处理 none 的情况。 这可以通过诸如 Option.getD 之类的辅助工具或使用模式匹配来完成。

def postalCodes : Std.HashMap Nat String := Std.HashMap.emptyWithCapacity 1 |>.insert 12345 "Schenectady" "not found"#eval postalCodes[12346]?.getD "not found" 
"not found"
"not found"#eval match postalCodes[12346]? with | none => "not found" | some city => city 
"not found"
"Schenectady"#eval if let some city := postalCodes[12345]? then city else "not found" 
"Schenectady"
在线查看 ↪
🔗归纳类型
Option.{u} (α : Type u) : Type u
Option.{u} (α : Type u) : Type u

可选值：要么是用 some 包裹的底层类型值，要么是 none。

对 Option 的 与 两种情形，结果按所述规则确定。

构造子

Option.none.{u} {α : Type u} : Option α

没有值。

Option.some.{u} {α : Type u} (val : α) : Option α

某个类型为 α 的值。

20.12.1. 强制转换🔗

从 α 到 Option α 存在一个强制转换，它会将值包装在 some 中。 这使得可以以类似于其他语言中可空类型的风格来使用 Option，在这些语言中，缺失的值由 none 指示，而存在的值没有特殊标记。

强制转换和 Option

在 getAlpha 中，读取了一行输入。 如果该行（在去掉开头和结尾的空格后）只由字母组成，则将其返回；否则，函数返回 none。

def getAlpha : IO (Option String) := do let line := (← (← IO.getStdin).getLine).`String.trim` has been deprecated: Use `String.trimAscii` instead Note: The updated constant has a different type: String → String.Slice instead of String → Stringtrim if line.length > 0 && line.all Char.isAlpha then return line else return none

在成功的情况下，没有显式地将 some 包装在 line 周围。 some 是由强制转换自动插入的。

在线查看 ↪

20.12.2. API 参考🔗

20.12.2.1. 提取值🔗

🔗定义
Option.get.{u} {α : Type u} (o : Option α) : o.isSome = true → α
Option.get.{u} {α : Type u}
  (o : Option α) : o.isSome = true → α

从可证明为 some 的可选值中提取其值。

🔗定义
Option.get!.{u} {α : Type u} [Inhabited α] : Option α → α
Option.get!.{u} {α : Type u}
  [Inhabited α] : Option α → α

从 Option 中提取值；遇到 none 时触发 panic。

🔗定义
Option.getD.{u_1} {α : Type u_1} (opt : Option α) (dflt : α) : α
Option.getD.{u_1} {α : Type u_1}
  (opt : Option α) (dflt : α) : α

取得可选值；遇到 none 时返回给定的默认值。

此段说明该操作的行为、边界条件及推荐用法。（相关项：@[macro_inline]、dflt、opt、none。）

以下列出相应示例或例外情况。

  • 示例见所列代码。（相关项：(some "hello").getD "goodbye" = "hello"。）

  • 示例见所列代码。（相关项：none.getD "goodbye" = "goodbye"。）

🔗定义
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 α

取得可选值；遇到 none 时以单子方式计算默认值。

它与所列操作对应或等价。（相关项：Option.getD。）

🔗定义
Option.getM.{u_1, u_2} {m : Type u_1 → Type u_2} {α : Type u_1}
  [Alternative m] : Option α → m α
Option.getM.{u_1, u_2}
  {m : Type u_1 → Type u_2} {α : Type u_1}
  [Alternative m] : Option α → m α

把可选值提升到任意 Alternative 中，并把 none 送到 failure。

🔗定义
Option.elim.{u_1, u_2} {α : Type u_1} {β : Sort u_2} :
  Option α → β → (α → β) → β
Option.elim.{u_1, u_2} {α : Type u_1}
  {β : Sort u_2} :
  Option α → β → (α → β) → β

对 Option 进行分类讨论的函数。

对 none 的 some 与 Option.elim 两种情形，结果按所述规则确定。（相关项：Option。）

对 Option.elim 的 Option 与 Option.recOn 两种情形，结果按所述规则确定。（相关项：Option.map、Option.getD、(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 β

对 Option 进行单子式分类讨论的函数。

对 none 的 some 与 Option.elimM 两种情形，结果按所述规则确定。（相关项：Option。）

它与所列操作对应或等价。（相关项：Option.elimM、Option.mapM、Option.getDM、Option.elim。）

🔗定义
Option.merge.{u_1} {α : Type u_1} (fn : α → α → α) :
  Option α → Option α → Option α
Option.merge.{u_1} {α : Type u_1}
  (fn : α → α → α) :
  Option α → Option α → Option α

若两个可选值都存在，则对它们应用函数；否则若仅有一个值存在，就返回该值且不使用函数。

对 some (fn a b) 的 some a 与 some b 两种情形，结果按所述规则确定。（相关项：Option.orElse、some x、some x、none、none、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。）

  • 示例见所列代码。（相关项：。）

  • 示例见所列代码。（相关项：。）

20.12.2.2. 属性和比较🔗

🔗定义
Option.isNone.{u_1} {α : Type u_1} : Option α → Bool
Option.isNone.{u_1} {α : Type u_1} :
  Option α → Bool

对 true 返回 none，对 false 返回 some x。

此段说明该操作的行为、边界条件及推荐用法。（相关项：(· == none)、BEq α。）

以下列出相应示例或例外情况。

🔗定义
Option.isSome.{u_1} {α : Type u_1} : Option α → Bool
Option.isSome.{u_1} {α : Type u_1} :
  Option α → Bool

对 true 返回 some x，对 false 返回 none。

🔗定义
Option.isEqSome.{u_1} {α : Type u_1} [BEq α] : Option α → α → Bool
Option.isEqSome.{u_1} {α : Type u_1}
  [BEq α] : Option α → α → Bool

检查可选值是否既存在又等于另一个值。

对 x? : Option α 的 y : α 与 x?.isEqSome y 两种情形，结果按所述规则确定。（相关项：x? == some y、、、。）

可选值的排序通常使用 DecidableEq (Option α)、LT (Option α)、Min (Option α) 和 Max (Option α) 实例。

🔗定义
Option.min.{u_1} {α : Type u_1} [Min α] : Option α → Option α → Option α
Option.min.{u_1} {α : Type u_1} [Min α] :
  Option α → Option α → Option α

两个可选值的最小值，并把 none 视为最小元素。（相关项：Min (Option α)。）

此段说明该操作的行为、边界条件及推荐用法。（相关项：nightly-2025-02-27、none、min none (some x) = min (some x) none = some x。）

以下列出相应示例或例外情况。

🔗定义
Option.max.{u_1} {α : Type u_1} [Max α] : Option α → Option α → Option α
Option.max.{u_1} {α : Type u_1} [Max α] :
  Option α → Option α → Option α

两个可选值的最大值。

通常通过所列实例、运算符或字段记法使用此函数。（相关项：Max (Option α)。）

以下列出相应示例或例外情况。

🔗定义
Option.lt.{u_1, u_2} {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :
  Option α → Option β → Prop
Option.lt.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (r : α → β → Prop) :
  Option α → Option β → Prop

把次序关系提升到 Option，并把 none 作为最小元素。

此段说明该操作的行为、边界条件及推荐用法。（相关项：none、α、β。）

对 LT (Option α) 的 Option.lt (fun n k : Nat => n < k) none none = False 与 Option.lt (fun n k : Nat => n < k) none (some 3) = True 两种情形，结果按所述规则确定。（相关项：Option.lt (fun n k : Nat => n < k) (some 3) none = False。）

以下列出相应示例或例外情况。

  • 示例见所列代码。（相关项：Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True。）

  • 示例见所列代码。（相关项：Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False。）

  • 示例见所列代码。（相关项：。）

  • 示例见所列代码。（相关项：。）

  • 示例见所列代码。（相关项：。）

🔗定义
Option.decidableEqNone.{u_1} {α : Type u_1} (o : Option α) :
  Decidable (o = none)
Option.decidableEqNone.{u_1}
  {α : Type u_1} (o : Option α) :
  Decidable (o = none)

即使被包裹类型没有可判定相等性，与 none 的相等性仍然可判定。

20.12.2.3. 转换🔗

🔗定义
Option.toArray.{u_1} {α : Type u_1} : Option α → Array α
Option.toArray.{u_1} {α : Type u_1} :
  Option α → Array α

把可选值转换为含零个或一个元素的数组。

以下列出相应示例或例外情况。

  • 示例见所列代码。（相关项：(some "value").toArray = #["value"]。）

  • 示例见所列代码。（相关项：none.toArray = #[]。）

🔗定义
Option.toList.{u_1} {α : Type u_1} : Option α → List α
Option.toList.{u_1} {α : Type u_1} :
  Option α → List α

把可选值转换为含零个或一个元素的列表。

以下列出相应示例或例外情况。

  • 示例见所列代码。（相关项：(some "value").toList = ["value"]。）

  • 示例见所列代码。（相关项：none.toList = []。）

🔗定义
Option.repr.{u_1} {α : Type u_1} [Repr α] : Option α → Nat → Std.Format
Option.repr.{u_1} {α : Type u_1}
  [Repr α] : Option α → Nat → Std.Format

返回可选值的一种表示，它应能被解析为等价的可选值。

通常通过所列实例、运算符或字段记法使用此函数。（相关项：Repr (Option α)。）

🔗定义
Option.format.{u} {α : Type u} [Std.ToFormat α] : Option α → Std.Format
Option.format.{u} {α : Type u}
  [Std.ToFormat α] : Option α → Std.Format

格式化可选值，不要求 Lean 解析器能够解析结果。

通常通过所列实例、运算符或字段记法使用此函数。（相关项：ToFormat (Option α)。）

20.12.2.4. 控制🔗

Option 可以被认为是描述一个可能无法返回值的计算。 Monad Option 实例以及 Alternative Option 正是基于这种理解。 返回 none 也可以被认为是抛出了一个不包含任何有用信息的异常，这被体现在 MonadExcept Unit Option 实例中。

🔗定义
Option.guard.{u_1} {α : Type u_1} (p : α → Bool) (a : α) : Option α
Option.guard.{u_1} {α : Type u_1}
  (p : α → Bool) (a : α) : Option α

若值不满足布尔谓词则返回 none，否则返回该值本身。

把 Option 看作可能失败的计算或至多含一个元素的容器时，此操作具有所述对应含义。（相关项：Option。）

以下列出相应示例或例外情况。

🔗定义
Option.bind.{u_1, u_2} {α : Type u_1} {β : Type u_2} :
  Option α → (α → Option β) → Option β
Option.bind.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} :
  Option α → (α → Option β) → Option β

对 Option 计算进行顺序组合。

把 Option 看作可能失败的计算或至多含一个元素的容器时，此操作具有所述对应含义。（相关项：Option。）

通常通过所列实例、运算符或字段记法使用此函数。（相关项：>>=、Bind (Option α)、do、相关说明。）

以下列出相应示例或例外情况。

🔗定义
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 β)

若 f 中存在值，则在该值上运行单子动作 o 并返回结果；否则返回 none。

把 Option 看作可能失败的计算或至多含一个元素的容器时，此操作具有所述对应含义。

🔗定义
Option.join.{u_1} {α : Type u_1} (x : Option (Option α)) : Option α
Option.join.{u_1} {α : Type u_1}
  (x : Option (Option α)) : Option α

展平嵌套的可选值，并保留其中找到的值。

它与所列操作对应或等价。（相关项：List.flatten。）

以下列出相应示例或例外情况。

🔗定义
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 α)

把可选的单子计算转换为返回可选值的单子计算。

此段说明该操作的行为、边界条件及推荐用法。（相关项：m。）

示例：

some "world"hello #eval show IO (Option String) from Option.sequence <| some do IO.println "hello" return "world" 
hello
some "world"
🔗定义
Option.tryCatch.{u_1} {α : Type u_1} (x : Option α)
  (handle : Unit → Option α) : Option α
Option.tryCatch.{u_1} {α : Type u_1}
  (x : Option α)
  (handle : Unit → Option α) : Option α

用处理函数从失败的 Option 计算中恢复。

通常通过所列实例、运算符或字段记法使用此函数。（相关项：MonadExceptOf Unit Option。）

以下列出相应示例或例外情况。

🔗定义
Option.or.{u_1} {α : Type u_1} : Option α → Option α → Option α
Option.or.{u_1} {α : Type u_1} :
  Option α → Option α → Option α

返回参数中第一个为 some 的值；若两者都不是 none 则返回 some。

此段说明该操作的行为、边界条件及推荐用法。（相关项：<|>、OrElse.orElse。）

🔗定义
Option.orElse.{u_1} {α : Type u_1} :
  Option α → (Unit → Option α) → Option α
Option.orElse.{u_1} {α : Type u_1} :
  Option α → (Unit → Option α) → Option α

为 OrElse 实现 <|> 的 Option 语法；若第一个参数是 some a 则返回 some a，否则求值并返回第二个参数。

可使用所列 API 完成检查、转换或采用更安全的替代方式。（相关项：or。）

20.12.2.5. 迭代🔗

Option 可以被认为是一个最多包含一个值的集合。 从这个角度来看，迭代运算符可以理解为对包含的值（如果存在）执行某些操作，如果不存在则什么也不做。

🔗定义
Option.all.{u_1} {α : Type u_1} (p : α → Bool) : Option α → Bool
Option.all.{u_1} {α : Type u_1}
  (p : α → Bool) : Option α → Bool

检查可选值是否为 none，或满足某个布尔谓词。

以下列出相应示例或例外情况。

  • 示例见所列代码。

  • 示例见所列代码。

  • 示例见所列代码。

🔗定义
Option.any.{u_1} {α : Type u_1} (p : α → Bool) : Option α → Bool
Option.any.{u_1} {α : Type u_1}
  (p : α → Bool) : Option α → Bool

检查可选值是否不是 none 且满足某个布尔谓词。

以下列出相应示例或例外情况。

  • 示例见所列代码。

  • 示例见所列代码。

  • 示例见所列代码。

🔗定义
Option.filter.{u_1} {α : Type u_1} (p : α → Bool) : Option α → Option α
Option.filter.{u_1} {α : Type u_1}
  (p : α → Bool) : Option α → Option α

仅当可选值满足布尔谓词时才保留它。

在所述条件下，函数按说明返回相应结果或后备结果。（相关项：Option、Option.filter、List.filter、Array.filter。）

以下列出相应示例或例外情况。

  • 示例见所列代码。（相关项：(some 5).filter (· % 2 == 0) = none。）

  • 示例见所列代码。（相关项：(some 4).filter (· % 2 == 0) = some 4。）

  • 示例见所列代码。（相关项：none.filter (fun x : Nat => x % 2 == 0) = none。）

  • 示例见所列代码。（相关项：none.filter (fun x : Nat => true) = none。）

🔗定义
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 α)

仅当可选值满足单子布尔谓词时才保留它。

在所述条件下，函数按说明返回相应结果或后备结果。（相关项：Option、Option.filterM、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 PUnit
Option.forM.{u_1, u_2, u_3}
  {m : Type u_1 → Type u_2} {α : Type u_3}
  [Pure m] :
  Option α → (α → m PUnit) → m PUnit

若可选值存在，则在其上执行单子动作；若不存在值则不做任何操作。

示例：

((), 5)#eval ((some 5).forM set : StateM Nat Unit).run 0 ((), 5)((), 0)#eval (none.forM (fun x : Nat => set x) : StateM Nat Unit).run 0 ((), 0)
🔗定义
Option.map.{u_1, u_2} {α : Type u_1} {β : Type u_2} (f : α → β) :
  Option α → Option β
Option.map.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (f : α → β) :
  Option α → Option β

若可选值存在，则对其应用函数。

把 Option 看作可能失败的计算或至多含一个元素的容器时，此操作具有所述对应含义。（相关项：List.map、Functor Option。）

以下列出相应示例或例外情况。

  • 示例见所列代码。（相关项：(none : Option Nat).map (· + 1) = none。）

  • 示例见所列代码。（相关项：(some 3).map (· + 1) = some 4。）

🔗定义
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 β)

把某个应用函子中的函数应用于可选值；若值缺失，则无效果地返回 none。

它与所列操作对应或等价。（相关项：Option.mapM。）

🔗定义
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 β)

把某个应用函子中的函数应用于可选值；若值缺失，则无效果地返回 none。

此段说明该操作的行为、边界条件及推荐用法。（相关项：f、none、none。）

把 Option 看作可能失败的计算或至多含一个元素的容器时，此操作具有所述对应含义。（相关项：List.mapM。）

它与所列操作对应或等价。（相关项：m、Option.mapA。）

20.12.2.6. 递归辅助🔗

🔗定义
Option.attach.{u_1} {α : Type u_1} (xs : Option α) :
  Option { x // xs = some x }
Option.attach.{u_1} {α : Type u_1}
  (xs : Option α) :
  Option { x // xs = some x }

为存在的可选值“附加”它确实就是该值的证明，并返回表达这一事实的子类型。

此函数主要用于良基递归的终止性证明，使迭代操作取得的值能与原参数建立所需关系。（相关项：Option.map。）

🔗定义
Option.attachWith.{u_1} {α : Type u_1} (xs : Option α) (P : α → Prop)
  (H : ∀ (x : α), xs = some x → P x) : Option { x // P x }
Option.attachWith.{u_1} {α : Type u_1}
  (xs : Option α) (P : α → Prop)
  (H : ∀ (x : α), xs = some x → P x) :
  Option { x // P x }

为存在的可选值“附加”某谓词成立的证明，并返回表达这一事实的子类型。

此函数主要用于良基递归的终止性证明，使迭代操作取得的值能与原参数建立所需关系。（相关项：Option.attach、Option.map。）

🔗定义
Option.unattach.{u_1} {α : Type u_1} {p : α → Prop}
  (o : Option { x // p x }) : Option α
Option.unattach.{u_1} {α : Type u_1}
  {p : α → Prop}
  (o : Option { x // p x }) : Option α

移除 Option 中的值确实就是该值的附加证明。

此函数主要用于良基递归的终止性证明，使迭代操作取得的值能与原参数建立所需关系。

在所述条件下，函数按说明返回相应结果或后备结果。（相关项：simp [Option.unattach, -Option.map_subtype]。）

它与所列操作对应或等价。（相关项：Option.map Subtype.val。）

20.12.2.7. 推理🔗

🔗定义
Option.choice.{u_1} (α : Type u_1) : Option α
Option.choice.{u_1} (α : Type u_1) :
  Option α

给定类型的一个可选任意元素。

在所述条件下，函数按说明返回相应结果或后备结果。（相关项：α、v : α、some v、none。）

🔗定义
Option.pbind.{u_1, u_2} {α : Type u_1} {β : Type u_2} (o : Option α)
  (f : (a : α) → o = some a → Option β) : Option β
Option.pbind.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} (o : Option α)
  (f : (a : α) → o = some a → Option β) :
  Option β

给定一个可选值以及仅当该值为 some 时才能应用的函数，在可能时返回应用该函数的结果。

运行时实现具有所述优化与复杂度特性。（相关项：f、a : α、o = some a、o、none、o、Option.bind。）

示例：

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
none
🔗定义
Option.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 → β) : β

给定一个可选值以及仅当该值为 some 时才能应用的函数，在可能时返回应用结果，否则返回后备值。

运行时实现具有所述优化与复杂度特性。（相关项：f、a : α、o = some a、o、none、o、Option.elim。）

示例：

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
none
🔗定义
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 β
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 β

给定从 α 中满足 p 的元素到 β 的函数，以及可选值存在时满足 p 的证明，把该函数应用于这个值。

示例：

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