Init.Data.Option.Basic

source

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

Option α → m α

Instances For

source

@[inline]

def Option.toBool {α : Type u_1} :

Option α → Bool

Instances For

source

@[inline]

def Option.isSome {α : Type u_1} :

Option α → Bool

Instances For

source

@[inline]

def Option.isNone {α : Type u_1} :

Option α → Bool

Instances For

source

@[inline]

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

Option α → α → Bool

Instances For

source

@[inline]

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

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

Instances For

source

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

Instances For

source

theorem Option.map_id {α : Type u_1} :

Option.map id = id

source

@[inline]

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

Option α → Option α

Instances For

source

@[inline]

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

Option α → Bool

Instances For

source

@[inline]

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

Option α → Bool

Instances For

source

@[macro_inline]

def Option.orElse {α : Type u_1} :

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

Instances For

source

instance Option.instOrElseOption {α : Type u_1} :

OrElse (Option α)

source

@[inline]

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

Option α → Option α → Prop

Instances For

source

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

DecidableRel (Option.lt r)

source

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.

Instances For

source

instance instDecidableEqOption :

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

source

instance instBEqOption :

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

source

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

LT (Option α)

source

@[always_inline]

instance instFunctorOption :

Functor Option

source

@[always_inline]

instance instMonadOption :

Monad Option

source

@[always_inline]

instance instAlternativeOption :

Alternative Option

source

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

Option α → m α

Instances For

source

@[inline]

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

Option α

Instances For

source

instance instMonadExceptOfUnitOption :

MonadExceptOf Unit Option