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