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.lean. 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
              @[deprecated Option.commutative_merge (since := "2025-06-03")]
              theorem Option.merge_isCommutative {α : Type u_1} (f : α → α → α) [Std.Commutative f] :
              Std.Commutative (merge f)
              source
              @[deprecated Option.associative_merge (since := "2025-06-03")]
              theorem Option.merge_isAssociative {α : Type u_1} (f : α → α → α) [Std.Associative f] :
              Std.Associative (merge f)
              source
              @[deprecated Option.idempotentOp_merge (since := "2025-06-03")]
              theorem Option.merge_isIdempotent {α : Type u_1} (f : α → α → α) [Std.IdempotentOp f] :
              Std.IdempotentOp (merge f)
              source
              @[deprecated Option.lawfulIdentity_merge (since := "2025-06-03")]
              theorem 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.