Init.Control.Option

source

instance instToBoolOption {α : Type u_1} :

ToBool (Option α)

Equations

instToBoolOption = { toBool := Option.toBool }

source

noncomputable def OptionT (m : Type u → Type v) (α : Type u) :

Type v

Equations

OptionT m α = m (Option α)

source

@[inline]

def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) :

m (Option α)

Equations

OptionT.run x = x

source

def OptionT.mk {m : Type u → Type v} {α : Type u} (x : m (Option α)) :

OptionT m α

Equations

OptionT.mk x = x

source

@[inline]

def OptionT.bind {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (x : OptionT m α) (f : α → OptionT m β) :

OptionT m β

Equations

OptionT.bind x f = OptionT.mk do let a ← x match a with | some a => f a | none => pure none

source

@[inline]

def OptionT.pure {m : Type u → Type v} [inst : Monad m] {α : Type u} (a : α) :

OptionT m α

Equations

OptionT.pure a = OptionT.mk (pure (some a))

source

instance OptionT.instMonadOptionT {m : Type u → Type v} [inst : Monad m] :

Monad (OptionT m)

Equations

OptionT.instMonadOptionT = Monad.mk

source

@[inline]

def OptionT.orElse {m : Type u → Type v} [inst : Monad m] {α : Type u} (x : OptionT m α) (y : Unit → OptionT m α) :

OptionT m α

Equations

OptionT.orElse x y = OptionT.mk do let a ← x match a with | some a => pure (some a) | x => y ()

source

@[inline]

def OptionT.fail {m : Type u → Type v} [inst : Monad m] {α : Type u} :

OptionT m α

Equations

OptionT.fail = OptionT.mk (pure none)

source

instance OptionT.instAlternativeOptionT {m : Type u → Type v} [inst : Monad m] :

Alternative (OptionT m)

Equations

OptionT.instAlternativeOptionT = Alternative.mk (fun {α} => OptionT.fail) fun {α} => OptionT.orElse

source

@[inline]

def OptionT.lift {m : Type u → Type v} [inst : Monad m] {α : Type u} (x : m α) :

OptionT m α

Equations

OptionT.lift x = OptionT.mk do let a ← x pure (some a)

source

instance OptionT.instMonadLiftOptionT {m : Type u → Type v} [inst : Monad m] :

MonadLift m (OptionT m)

Equations

OptionT.instMonadLiftOptionT = { monadLift := fun {α} => OptionT.lift }

source

instance OptionT.instMonadFunctorOptionT {m : Type u → Type v} :

MonadFunctor m (OptionT m)

Equations

OptionT.instMonadFunctorOptionT = { monadMap := fun {α} f x => f (Option α) x }

source

@[inline]

def OptionT.tryCatch {m : Type u → Type v} [inst : Monad m] {α : Type u} (x : OptionT m α) (handle : Unit → OptionT m α) :

OptionT m α

Equations

OptionT.tryCatch x handle = OptionT.mk do let discr ← x match discr with | some a => pure (some a) | x => handle ()

source

instance OptionT.instMonadExceptOfUnitOptionT {m : Type u → Type v} [inst : Monad m] :

MonadExceptOf Unit (OptionT m)

Equations

OptionT.instMonadExceptOfUnitOptionT = { throw := fun {α} x => OptionT.fail, tryCatch := fun {α} => OptionT.tryCatch }

source

instance OptionT.instMonadExceptOfOptionT {m : Type u → Type v} (ε : Type u) [inst : Monad m] [inst : MonadExceptOf ε m] :

MonadExceptOf ε (OptionT m)

Equations

OptionT.instMonadExceptOfOptionT ε = { throw := fun {α} e => OptionT.mk (throwThe ε e), tryCatch := fun {α} x handle => OptionT.mk (tryCatchThe ε x handle) }

source

@[inline]

abbrev OptionM (α : Type u) :

Type u

Equations

OptionM α = OptionT Id α

source

@[inline]

abbrev OptionM.run {α : Type u_1} (x : OptionM α) :

Option α

Equations

OptionM.run x = x

source

instance instMonadControlOptionT {m : Type u_1 → Type u_2} [inst : Monad m] :

MonadControl m (OptionT m)

Equations

instMonadControlOptionT = { stM := Option, liftWith := fun {α} f => liftM (f fun {β} x => OptionT.run x), restoreM := fun {α} x => x }

source

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

Option α → m α

Equations

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