def Lake.OptionIO : Type → Type

Conceptually identical to OptionT BaseIO, but practically more efficient.

Equations

• Lake.OptionIO = EIO PUnit

instance Lake.instMonadOptionIO : Monad Lake.OptionIO

Equations

• Lake.instMonadOptionIO = inferInstanceAs (Monad (EIO PUnit))

instance Lake.instMonadLiftBaseIOOptionIO : MonadLift BaseIO Lake.OptionIO

Equations

• Lake.instMonadLiftBaseIOOptionIO = inferInstanceAs (MonadLift BaseIO (EIO PUnit))

@[inline]

def Lake.OptionIO.mk {α : Type} (x : EIO PUnit α) : Lake.OptionIO α

Equations

• Lake.OptionIO.mk x = x

@[inline]

def Lake.OptionIO.toBaseIO {α : Type} (self : Lake.OptionIO α) : BaseIO (Option α)

Equations

• Lake.OptionIO.toBaseIO self s = match self s with | EStateM.Result.ok a s => EStateM.Result.ok (some a) s | EStateM.Result.error a s => EStateM.Result.ok none s

@[inline]

def Lake.OptionIO.toEIO {α : Type} (self : Lake.OptionIO α) : EIO PUnit α

Equations

• Lake.OptionIO.toEIO self = self

@[inline]

def Lake.OptionIO.toIO {α : Type} (f : Unit → IO.Error) (self : Lake.OptionIO α) : IO α

Equations

• Lake.OptionIO.toIO f self = EIO.toIO f (Lake.OptionIO.toEIO self)

@[inline]

def Lake.OptionIO.catchFailure {α : Type} (f : Unit → BaseIO α) (self : Lake.OptionIO α) : BaseIO α

Equations

• Lake.OptionIO.catchFailure f self = EIO.catchExceptions (Lake.OptionIO.toEIO self) f

@[inline]

def Lake.OptionIO.failure {α : Type} : Lake.OptionIO α

Equations

• Lake.OptionIO.failure = Lake.OptionIO.mk (throw ())

@[inline]

def Lake.OptionIO.orElse {α : Type} (self : Lake.OptionIO α) (f : Unit → Lake.OptionIO α) : Lake.OptionIO α

Equations

• Lake.OptionIO.orElse self f = Lake.OptionIO.mk (tryCatch (Lake.OptionIO.toEIO self) f)

instance Lake.OptionIO.instAlternativeOptionIO : Alternative Lake.OptionIO

Equations

• Lake.OptionIO.instAlternativeOptionIO = Alternative.mk (fun {α : Type} => Lake.OptionIO.failure) fun {α : Type} => Lake.OptionIO.orElse

@[always_inline]

instance Lake.OptionIO.OptionIO.finally : MonadFinally Lake.OptionIO

Equations

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

@[inline]

def Lake.OptionIO.asTask {α : Type} (self : Lake.OptionIO α) (prio : optParam Task.Priority Task.Priority.dedicated) : BaseIO (Task (Option α))

Equations

• Lake.OptionIO.asTask self prio = BaseIO.asTask (Lake.OptionIO.toBaseIO self) prio