Documentation

Std.Data.Option.Basic

def Option.elim {α : Type u_1} {β : Sort u_2} :
Option αβ(αβ) → β

An elimination principle for Option. It is a nondependent version of Option.recOn.

Equations
  • Option.elim x x x = match x, x, x with | some x, x_1, f => f x | none, y, x => y
instance Option.instMembershipOption {α : Type u_1} :
Equations
  • Option.instMembershipOption = { mem := fun a b => b = some a }
@[simp]
theorem Option.mem_def {α : Type u_1} {a : α} {b : Option α} :
a b b = some a
theorem Option.isNone_iff_eq_none {α : Type u_1} {o : Option α} :
theorem Option.some_inj {α : Type u_1} {a : α} {b : α} :
some a = some b a = b
@[inline]
def Option.decidable_eq_none {α : Type u_1} {o : Option α} :
Decidable (o = none)

o = 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 instance : DecidableEq Option. Try to use o.isNone or o.isSome instead.

Equations
instance Option.instForAllOptionDecidableForAllMemInstMembershipOption {α : Type u_1} {p : αProp} [inst : DecidablePred p] (o : Option α) :
Decidable ((a : α) → a op a)
Equations
  • One or more equations did not get rendered due to their size.
instance Option.instForAllOptionDecidableExistsAndMemInstMembershipOption {α : Type u_1} {p : αProp} [inst : DecidablePred p] (o : Option α) :
Decidable (a, a o p a)
Equations
  • One or more equations did not get rendered due to their size.
def Option.get {α : Type u} (o : Option α) :

Extracts the value a from an option that is known to be some a for some a.

Equations
def Option.guard {α : Type u_1} (p : αProp) [inst : DecidablePred p] (a : α) :

guard p a returns some a if p a holds, otherwise none.

Equations
def Option.toList {α : Type u_1} :
Option αList α

Cast of Option to List. Returns [a] if the input is some a, and [] if it is none.

Equations
def Option.toArray {α : Type u_1} :
Option αArray α

Cast of Option to Array. Returns [a] if the input is some a, and [] if it is none.

Equations
def Option.liftOrGet {α : Type u_1} (f : ααα) :
Option αOption αOption α

Two arguments failsafe function. Returns f a b if the inputs are some a and some b, and "does nothing" otherwise.

Equations
inductive Option.Rel {α : Type u_1} {β : Type u_2} (r : αβProp) :
Option αOption βProp

Lifts a relation α → β → Prop→ β → Prop→ Prop to a relation Option α → Option β → Prop→ Option β → Prop→ Prop by just adding none ~ none.

Instances For
    def Option.pbind {α : Type u_1} {β : Type u_2} (x : Option α) :
    ((a : α) → a xOption β) → Option β

    Partial bind. If for some x : Option α, f : Π (a : α), a ∈ x → Option β∈ x → Option β→ Option β is a partial function defined on a : α giving an Option β, where some a = x, then pbind x f h is essentially the same as bind x f but is defined only when all x = some a, using the proof to apply f.

    Equations
    def Option.pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (x : Option α) :
    ((a : α) → a xp a) → Option β

    Partial map. If f : Π a, p a → β→ β is a partial function defined on a : α satisfying p, then pmap f x h is essentially the same as map f x but is defined only when all members of x satisfy p, using the proof to apply f.

    Equations
    @[inline]
    def Option.join {α : Type u_1} (x : Option (Option α)) :

    Flatten an Option of Option, a specialization of joinM.

    Equations
    def Option.forM {m : TypeType u_1} {α : Type u_2} [inst : Pure m] :
    Option α(αm PUnit) → m PUnit

    Map a monadic function which returns Unit over an Option.

    Equations
    instance Option.instForMOption {m : TypeType u_1} {α : Type u_2} :
    ForM m (Option α) α
    Equations
    • Option.instForMOption = { forM := fun [Monad m] => Option.forM }
    instance Option.instForIn'OptionInferInstanceMembershipInstMembershipOption {m : Type u_1 → Type u_2} {α : Type u_3} :
    ForIn' m (Option α) α inferInstance
    Equations
    • One or more equations did not get rendered due to their size.
    def Option.mapA {m : Type u_1 → Type u_2} [inst : Applicative m] {α : Type u_3} {β : Type u_1} (f : αm β) :
    Option αm (Option β)

    Like Option.mapM but for applicative functors.

    Equations
    def Option.sequence {m : Type u → Type u_1} [inst : Monad m] {α : Type u} :
    Option (m α)m (Option α)

    If you maybe have a monadic computation in a [Monad m] which produces a term of type α, then there is a naturally associated way to always perform a computation in m which maybe produces a result.

    Equations
    @[inline]
    def Option.elimM {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [inst : Monad m] (x : m (Option α)) (y : m β) (z : αm β) :
    m β

    A monadic analogue of Option.elim.

    Equations
    @[inline]
    def Option.getDM {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : Option α) (y : m α) :
    m α

    A monadic analogue of Option.getD.

    Equations