Documentation

Mathlib.Data.Option.Defs

Extra definitions on Option #

This file defines more operations involving Option α. Lemmas about them are located in other files under Mathlib.Data.Option. Other basic operations on Option are defined in the core library.

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.traverse {F : Type u → Type v} [inst : Applicative F] {α : Type u_1} {β : Type u} (f : αF β) :
    Option αF (Option β)

    Traverse an object of Option α with a function f : α → F β→ F β for an applicative F.

    Equations
    def Option.maybe {m : Type u → Type v} [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
    def Option.getDM' {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : m (Option α)) (y : m α) :
    m α
    Equations
    def Option.elim' {α : Type u_1} {β : Type u_2} (b : β) (f : αβ) :
    Option αβ

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

    Equations
    theorem Option.mem_some_iff {α : Type u_1} {a : α} {b : α} :
    a some b b = a
    @[inline]
    def Option.decidableEqNone {α : 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 Option.decidableEq. Try to use o.isNone or o.isSome instead.

    Equations
    instance Option.decidableForallMem {α : 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.decidableExistsMem {α : 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.iget {α : Type u_1} [inst : Inhabited α] :
    Option αα

    Inhabited get function. Returns a if the input is some a, otherwise returns default.

    Equations
    theorem Option.iget_some {α : Type u_1} [inst : Inhabited α] {a : α} :
    @[simp]
    theorem Option.mem_toList {α : Type u_1} {a : α} {o : Option α} :