doc-next-gen

Init.Data.Option.Instances

Module docstring

{}

Option.instMembership instance
: Membership α (Option α)
Full source 
instance : Membership α (Option α) := ⟨fun b a => b = some a⟩
Membership in Optional Values
Informal description
For any type $\alpha$, the membership relation $a \in o$ for $a \in \alpha$ and $o$ an optional value of type $\alpha$ holds if and only if $o$ is `some a`.
Option.mem_def theorem
{a : α} {b : Option α} : a ∈ b ↔ b = some a
Full source 
@[simp] theorem mem_def {a : α} {b : Option α} : a ∈ ba ∈ b ↔ b = some a := .rfl
Membership in Optional Values: $a \in b \leftrightarrow b = \text{some}\ a$
Informal description
For any element $a$ of type $\alpha$ and any optional value $b$ of type $\text{Option}\ \alpha$, the membership relation $a \in b$ holds if and only if $b$ is equal to $\text{some}\ a$.
Option.instDecidableMemOfDecidableEq instance
[DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o)
Full source 
instance [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o) :=
  inferInstanceAs <| Decidable (o = some j)
Decidability of Membership in Optional Values
Informal description
For any type $\alpha$ with decidable equality, and for any element $j \in \alpha$ and optional value $o \in \text{Option}\ \alpha$, the proposition $j \in o$ is decidable.
Option.some_inj theorem
{a b : α} : some a = some b ↔ a = b
Full source 
theorem some_inj {a b : α} : somesome a = some b ↔ a = b := by simp; rfl
Injectivity of the `some` constructor for optional values: $\text{some}(a) = \text{some}(b) \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the equality $\text{some}(a) = \text{some}(b)$ holds if and only if $a = b$.
Option.decidable_eq_none definition
{o : Option α} : Decidable (o = none)
Full source 
/--
Equality with `none` is decidable even if the wrapped type does not have decidable equality.

This is not an instance because it is not definitionally equal to the standard instance of
`DecidableEq (Option α)`, which can cause problems. It can be locally bound if needed.

Try to use the Boolean comparisons `Option.isNone` or `Option.isSome` instead.
-/
@[inline] def decidable_eq_none {o : Option α} : Decidable (o = none) :=
  decidable_of_decidable_of_iff isNone_iff_eq_none
Decidability of equality with `none` for optional values
Informal description
For any optional value `o` of type `Option α`, the equality `o = none` is decidable. This is constructed by using the bi-implication between `o.isNone` and `o = none`, and the decidability of `o.isNone`.
Option.instDecidableForallForallMemOfDecidablePred instance
{p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (∀ a, a ∈ o → p a)
Full source 
instance {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (∀ a, a ∈ o → p a)
| none => isTrue nofun
| some a =>
  if h : p a then isTrue fun _ e => some_inj.1 e ▸ h
  else isFalse <| mt (· _ rfl) h
Decidability of Universal Quantification over Optional Values
Informal description
For any decidable predicate $p$ on a type $\alpha$ and any optional value $o$ of type $\alpha$, the proposition that for all $a \in \alpha$, if $a$ is in $o$ then $p(a)$ holds is decidable.
Option.instDecidableExistsAndMemOfDecidablePred instance
{p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (Exists fun a => a ∈ o ∧ p a)
Full source 
instance {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (Exists fun a => a ∈ oa ∈ o ∧ p a)
| none => isFalse nofun
| some a => if h : p a then isTrue ⟨_, rfl, h⟩ else isFalse fun ⟨_, ⟨rfl, hn⟩⟩ => h hn
Decidability of Existential Quantification over Optional Values
Informal description
For any type $\alpha$ and decidable predicate $p$ on $\alpha$, and for any optional value $o : \text{Option }\alpha$, the proposition $\exists a \in o, p(a)$ is decidable. That is, we can constructively determine whether there exists an element $a$ in $o$ such that $p(a)$ holds.
Option.pbind definition
: (o : Option α) → (f : (a : α) → a ∈ o → Option β) → Option β
Full source 
/--
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 `a ∈ o`, which
is equivalent to `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:
```lean example
def attach (v : Option α) : Option { y : α // y ∈ v } :=
  v.pbind fun x h => some ⟨x, h⟩
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
-/
@[inline]
def pbind : (o : Option α) → (f : (a : α) → a ∈ o → Option β) → Option β
  | none, _ => none
  | some a, f => f a rfl
Partial bind for optional values
Informal description
Given an optional value `o : Option α` and a partial function `f : (a : α) → a ∈ o → Option β`, the function `Option.pbind` returns `none` if `o` is `none`, or applies `f` to the value `a` inside `some a` (along with a proof that `a ∈ o`) if `o` is `some a`.
Option.pmap definition
{p : α → Prop} (f : ∀ a : α, p a → β) : (o : Option α) → (∀ a, a ∈ o → p a) → Option β
Full source 
/--
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:
```lean example
def attach (v : Option α) : Option { y : α // y ∈ v } :=
  v.pmap (fun a (h : a ∈ v) => ⟨_, h⟩) (fun _ h => h)
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
-/
@[inline] def pmap {p : α → Prop}
    (f : ∀ a : α, p a → β) :
    (o : Option α) → (∀ a, a ∈ o → p a) → Option β
  | none, _ => none
  | some a, H => f a (H a rfl)
Partial map on optional values
Informal description
Given a predicate `p` on elements of type `α`, a function `f` that maps elements of `α` satisfying `p` to elements of type `β`, and an optional value `o : Option α` with a proof that all elements in `o` satisfy `p`, the function `Option.pmap` applies `f` to the value inside `o` if it is present (i.e., `some a`), or returns `none` if `o` is `none`.
Option.pelim definition
(o : Option α) (b : β) (f : (a : α) → a ∈ o → β) : β
Full source 
/--
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 `a ∈ o`, which
is equivalent to `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:
```lean example
def attach (v : Option α) : Option { y : α // y ∈ v } :=
  v.pelim none fun x h => some ⟨x, h⟩
```
```lean example
#reduce attach (some 3)
```
```output
some ⟨3, ⋯⟩
```
```lean example
#reduce attach none
```
```output
none
```
-/
@[inline] def pelim (o : Option α) (b : β) (f : (a : α) → a ∈ o → β) : β :=
  match o with
  | none => b
  | some a => f a rfl
Partial elimination of an optional value
Informal description
Given an optional value `o : Option α`, a fallback value `b : β`, and a partial function `f : (a : α) → a ∈ o → β`, the function `Option.pelim` returns `b` if `o` is `none`, or applies `f` to the value `a` inside `some a` along with a proof that `a ∈ o` if `o` is `some a`.
Option.forM definition
[Pure m] : Option α → (α → m PUnit) → m PUnit
Full source 
/--
Executes a monadic action on an optional value if it is present, or does nothing if there is no
value.

Examples:
```lean example
#eval ((some 5).forM set : StateM Nat Unit).run 0
```
```output
((), 5)
```
```lean example
#eval (none.forM (fun x : Nat => set x) : StateM Nat Unit).run 0
```
```output
((), 0)
```
-/
@[inline] protected def forM [Pure m] : Option α → (α → m PUnit) → m PUnit
  | none  , _ => pure ⟨⟩
  | some a, f => f a
Monadic action on optional value
Informal description
Given a monadic action `f : α → m PUnit` and an optional value `o : Option α`, the function `Option.forM` applies `f` to the value inside `o` if it is present (i.e., `some a`), or does nothing (returns `pure ⟨⟩`) if `o` is `none`.
Option.instForM instance
: ForM m (Option α) α
Full source 
instance : ForM m (Option α) α :=
  ⟨Option.forM⟩
Monadic Iteration over Optional Values
Informal description
For any monad `m` and type `α`, the type `Option α` can be equipped with a `ForM` instance, allowing monadic iteration over optional values. This means that for an optional value `o : Option α`, one can perform a monadic action on the contained value if it exists (`some a`), or do nothing if it is `none`.
Option.instForIn'InferInstanceMembership instance
: ForIn' m (Option α) α inferInstance
Full source 
instance : ForIn' m (Option α) α inferInstance where
  forIn' x init f := do
    match x with
    | none => return init
    | some a =>
      match ← f a rfl init with
      | .done r | .yield r => return r
Monadic Iteration with Membership Proofs for Optional Values
Informal description
For any monad `m` and type `α`, the type `Option α` can be equipped with a `ForIn'` instance, enabling monadic iteration over optional values with membership proofs. This allows the use of `for h : x in o` notation where `o : Option α`, where `h` provides a proof that `x` is the contained value when `o` is `some x`.