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

Equations

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

@[inline]

def Option.toBool {α : Type u_1} : Option α → Bool

Equations

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

@[inline]

def Option.isSome {α : Type u_1} : Option α → Bool

Equations

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

@[inline]

def Option.isNone {α : Type u_1} : Option α → Bool

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

theorem Option.map_id {α : Type u_1} : Option.map id = id

@[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

@[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

@[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

@[macro_inline]

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 ()

instance Option.instOrElseOption {α : Type u_1} : OrElse (Option α)

Equations

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

@[inline]

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.

def Option.merge {α : Type u_1} (fn : α → α → α) : Option α → Option α → Option α

Take a pair of options and if they are both some, apply the given fn to produce an output. Otherwise act like orElse.

Equations

• Option.merge fn x✝ x = match x✝, x with | none, none => none | some x, none => some x | none, some y => some y | some x, some y => some (fn x y)

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

Equations

• instDecidableEqOption = decEqOption✝

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

Equations

• instBEqOption = { beq := beqOption✝ }

instance instLTOption {α : Type u_1} [LT α] : LT (Option α)

Equations

• instLTOption = { lt := Option.lt fun (x x_1 : α) => x < x_1 }

@[always_inline]

instance instFunctorOption : Functor Option

Equations

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

@[always_inline]

instance instMonadOption : Monad Option

Equations

• instMonadOption = Monad.mk

@[always_inline]

instance instAlternativeOption : Alternative Option

Equations

• instAlternativeOption = Alternative.mk (fun {α : Type u_1} => none) fun {α : Type u_1} => Option.orElse

def liftOption {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] : Option α → m α

Equations

• liftOption x = match x with | some a => pure a | none => failure

@[inline]

def Option.tryCatch {α : Type u_1} (x : Option α) (handle : Unit → Option α) : Option α

Equations

• Option.tryCatch x handle = match x with | some val => x | none => handle ()

instance instMonadExceptOfUnitOption : MonadExceptOf Unit Option

Equations

• instMonadExceptOfUnitOption = { throw := fun {α : Type u_1} (x : Unit) => none, tryCatch := fun {α : Type u_1} => Option.tryCatch }