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.

source
def Option.traverse {F : Type u → Type v} [Applicative F] {α : Type u_1} {β : Type u} (f : α → F β) :
Option α → F (Option β)

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

Equations
Instances For
    source
    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
    Instances For
      source
      @[simp]
      theorem Option.elim'_none {α : Type u_1} {β : Type u_2} (b : β) (f : α → β) :
      Option.elim' b f none = b
      source
      @[simp]
      theorem Option.elim'_some {α : Type u_1} {β : Type u_2} {a : α} (b : β) (f : α → β) :
      Option.elim' b f (some a) = f a
      source
      @[simp]
      theorem Option.elim'_none_some {α : Type u_1} {β : Type u_2} (f : Option α → β) :
      Option.elim' (f none) (f ∘ some) = f
      source
      theorem Option.elim'_eq_elim {α : Type u_3} {β : Type u_4} (b : β) (f : α → β) (a : Option α) :
      Option.elim' b f a = a.elim b f
      source
      @[reducible, inline]
      abbrev Option.iget {α : Type u_1} [Inhabited α] :
      Option α → α

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

      Equations
      Instances For
        source
        theorem Option.iget_some {α : Type u_1} [Inhabited α] {a : α} :
        (some a).iget = a
        source
        instance Option.merge_isCommutative {α : Type u_1} (f : α → α → α) [Std.Commutative f] :
        Std.Commutative (merge f)
        source
        instance Option.merge_isAssociative {α : Type u_1} (f : α → α → α) [Std.Associative f] :
        Std.Associative (merge f)
        source
        instance Option.merge_isIdempotent {α : Type u_1} (f : α → α → α) [Std.IdempotentOp f] :
        Std.IdempotentOp (merge f)
        source
        instance Option.merge_isId {α : Type u_1} (f : α → α → α) :
        Std.LawfulIdentity (merge f) none
        source
        @[deprecated Option.merge_isCommutative (since := "2025-04-04")]
        theorem Option.liftOrGet_isCommutative {α : Type u_1} (f : α → α → α) [Std.Commutative f] :
        Std.Commutative (merge f)

        Alias of Option.merge_isCommutative.

        source
        @[deprecated Option.merge_isAssociative (since := "2025-04-04")]
        theorem Option.liftOrGet_isAssociative {α : Type u_1} (f : α → α → α) [Std.Associative f] :
        Std.Associative (merge f)

        Alias of Option.merge_isAssociative.

        source
        @[deprecated Option.merge_isIdempotent (since := "2025-04-04")]
        theorem Option.liftOrGet_isIdempotent {α : Type u_1} (f : α → α → α) [Std.IdempotentOp f] :
        Std.IdempotentOp (merge f)

        Alias of Option.merge_isIdempotent.

        source
        @[deprecated Option.merge_isId (since := "2025-04-04")]
        theorem Option.liftOrGet_isId {α : Type u_1} (f : α → α → α) :
        Std.LawfulIdentity (merge f) none

        Alias of Option.merge_isId.