Init.Data.Option.Basic

source

def Option.toMonad {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [inst : Alternative m] :

Option α → m α

Equations

Option.toMonad x = match x with | none => failure | some a => pure a

source

@[inline]

def Option.toBool {α : Type u_1} :

Option α → Bool

Equations

Option.toBool x = match x with | some x => true | none => false

source

@[inline]

def Option.isSome {α : Type u_1} :

Option α → Bool

Equations

Option.isSome x = match x with | some x => true | none => false

source

@[inline]

def Option.isNone {α : Type u_1} :

Option α → Bool

Equations

Option.isNone x = match x with | some x => false | none => true

source

@[inline]

def Option.isEqSome {α : Type u_1} [inst : BEq α] :

Option α → α → Bool

Equations

Option.isEqSome x x = match x, x with | some a, b => a == b | none, x => false

source

@[inline]

def Option.bind {α : Type u_1} {β : Type u_2} :

Option α → (α → Option β) → Option β

Equations

Option.bind x x = match x, x with | none, b => none | some a, b => b a

source

@[inline]

def Option.map {α : Type u_1} {β : Type u_2} (f : α → β) (o : Option α) :

Option β

Equations

Option.map f o = Option.bind o (some ∘ f)

source

@[inline]

def Option.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → m β) (o : Option α) :

m (Option β)

Equations

Option.mapM f o = match o with | some a => do let a ← f a pure (some a) | x => pure none

source

theorem Option.map_id {α : Type u_1} :

Option.map id = id

source

instance Option.instFunctorOption :

Functor Option

Equations

Option.instFunctorOption = { map := fun {α β} => Option.map, mapConst := fun {α β} => Option.map ∘ Function.const β }

source

@[inline]

def Option.filter {α : Type u_1} (p : α → Bool) :

Option α → Option α

Equations

Option.filter p x = match x with | some a => if p a = true then some a else none | none => none

source

@[inline]

def Option.all {α : Type u_1} (p : α → Bool) :

Option α → Bool

Equations

Option.all p x = match x with | some a => p a | none => true

source

@[inline]

def Option.any {α : Type u_1} (p : α → Bool) :

Option α → Bool

Equations

Option.any p x = match x with | some a => p a | none => false

source

@[macroInline]

def Option.orElse {α : Type u_1} :

Option α → (Unit → Option α) → Option α

Equations

Option.orElse x x = match x, x with | some a, x => some a | none, b => b ()

source

instance Option.instOrElseOption {α : Type u_1} :

OrElse (Option α)

Equations

Option.instOrElseOption = { orElse := Option.orElse }

source

@[inline]

noncomputable def Option.lt {α : Type u_1} (r : α → α → Prop) :

Option α → Option α → Prop

Equations

Option.lt r x x = match x, x with | none, some x => True | some x, some y => r x y | x, x_1 => False

source

instance Option.instDecidableRelOptionLt {α : Type u_1} (r : α → α → Prop) [s : DecidableRel r] :

DecidableRel (Option.lt r)

Equations

Option.instDecidableRelOptionLt r x x = match x, x with | none, some y => isTrue trivial | some x, some y => s x y | some x, none => isFalse not_false | none, none => isFalse not_false

source

instance instDecidableEqOption :

{α : Type u_1} → [inst : DecidableEq α] → DecidableEq (Option α)

Equations

instDecidableEqOption = [anonymous]

source

instance instBEqOption :

{α : Type u_1} → [inst : BEq α] → BEq (Option α)

Equations

instBEqOption = { beq := [anonymous] }

source

instance instLTOption {α : Type u_1} [inst : LT α] :

LT (Option α)

Equations

instLTOption = { lt := Option.lt fun a a_1 => a < a_1 }