inductive Lake.EResult (ε : Type u) (σ : Type v) (α : Type w) : Type (max u v w)

EResult ε σ α is equivalent to Except ε α × σ, but using a single combined inductive yields a more efficient data representation.

This is a universe-polymorphic version of EStateM.Result.

• ok {ε : Type u} {σ : Type v} {α : Type w} : α → σ → EResult ε σ α

  A success value of type α, and a new state σ.

• error {ε : Type u} {σ : Type v} {α : Type w} : ε → σ → EResult ε σ α

  A failure value of type ε, and a new state σ.

instance Lake.instInhabitedEResult {α : Type u_1} {σ : Type u_2} {ε : Type u_3} [Inhabited α] [Inhabited σ] : Inhabited (EResult ε σ α)

Equations

• Lake.instInhabitedEResult = { default := Lake.EResult.ok default default }

instance Lake.instInhabitedEResult_1 {ε : Type u_1} {σ : Type u_2} {α : Type u_3} [Inhabited ε] [Inhabited σ] : Inhabited (EResult ε σ α)

Equations

• Lake.instInhabitedEResult_1 = { default := Lake.EResult.error default default }

@[inline]

def Lake.EResult.state {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → σ

Extract the state σ from a EResult ε σ α.

Equations

• (Lake.EResult.ok a s).state = s
• (Lake.EResult.error a s).state = s

@[inline]

def Lake.EResult.modifyState {σ : Type u_1} {σ' : Type u_2} {ε : Type u_3} {α : Type u_4} (f : σ → σ') : EResult ε σ α → EResult ε σ' α

Equations

• Lake.EResult.modifyState f (Lake.EResult.ok a s) = Lake.EResult.ok a (f s)
• Lake.EResult.modifyState f (Lake.EResult.error e s) = Lake.EResult.error e (f s)

@[inline]

def Lake.EResult.setState {σ' : Type u_1} {ε : Type u_2} {σ : Type u_3} {α : Type u_4} (s : σ') (r : EResult ε σ α) : EResult ε σ' α

Equations

• Lake.EResult.setState s r = Lake.EResult.modifyState (fun (x : σ) => s) r

@[inline]

def Lake.EResult.toProd {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Except ε α × σ

Convert a EResult ε σ α into Except ε α × σ.

Equations

• (Lake.EResult.ok a s).toProd = (Except.ok a, s)
• (Lake.EResult.error a s).toProd = (Except.error a, s)

@[inline]

def Lake.EResult.toProd? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Option α × σ

Convert an EResult ε σ α into Option α × σ, discarding the exception contents.

Equations

• (Lake.EResult.ok a s).toProd? = (some a, s)
• (Lake.EResult.error a s).toProd? = (none, s)

@[inline]

def Lake.EResult.result? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Option α

Extract the result α from a EResult ε σ α.

Equations

• (Lake.EResult.ok a a_1).result? = some a
• x✝.result? = none

@[inline]

def Lake.EResult.error? {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Option ε

Extract the error ε from a EResult ε σ α.

Equations

• (Lake.EResult.error e a).error? = some e
• x✝.error? = none

@[inline]

def Lake.EResult.toExcept {ε : Type u_1} {σ : Type u_2} {α : Type u_3} : EResult ε σ α → Except ε α

Convert an EResult ε σ α into Except ε α, discarding its state.

Equations

• (Lake.EResult.ok a s).toExcept = Except.ok a
• (Lake.EResult.error a s).toExcept = Except.error a

@[inline]

def Lake.EResult.map {α : Type u_1} {β : Type u_2} {ε : Type u_3} {σ : Type u_4} (f : α → β) : EResult ε σ α → EResult ε σ β

Equations

• Lake.EResult.map f (Lake.EResult.ok a s) = Lake.EResult.ok (f a) s
• Lake.EResult.map f (Lake.EResult.error e s) = Lake.EResult.error e s

instance Lake.instFunctorEResult {ε : Type u_1} {σ : Type u_2} : Functor (EResult ε σ)

Equations

• Lake.instFunctorEResult = { map := fun {α β : Type ?u.19} => Lake.EResult.map }

def Lake.EResult.toEStateMResult {ε σ α : Type u_1} : EResult ε σ α → EStateM.Result ε σ α

Equations

• (Lake.EResult.ok a s).toEStateMResult = EStateM.Result.ok a s
• (Lake.EResult.error e s).toEStateMResult = EStateM.Result.error e s

def Lake.EResult.ofEStateMResult {ε σ α : Type u_1} : EStateM.Result ε σ α → EResult ε σ α

Equations

• Lake.EResult.ofEStateMResult (EStateM.Result.ok a s) = Lake.EResult.ok a s
• Lake.EResult.ofEStateMResult (EStateM.Result.error e s) = Lake.EResult.error e s

def Lake.EStateT (ε : Type u) (σ : Type v) (m : Type (max u v w) → Type x) (α : Type w) : Type (max v x)

EStateT ε σ m is a combined error and state monad transformer, equivalent to ExceptT ε (StateT σ m) but more efficient.

Equations

• Lake.EStateT ε σ m α = (σ → m (Lake.EResult ε σ α))

instance Lake.EStateT.instInhabitedOfPure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Inhabited ε] [Pure m] : Inhabited (EStateT ε σ m α)

Equations

• Lake.EStateT.instInhabitedOfPure = { default := fun (s : σ) => pure (Lake.EResult.error default s) }

@[inline]

def Lake.EStateT.run {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max u v w) → Type u_1} (init : σ) (self : EStateT ε σ m α) : m (EResult ε σ α)

Execute an EStateT on initial state init to get an EResult result.

Equations

• Lake.EStateT.run init self = self init

@[inline]

def Lake.EStateT.run' {ε : Type u} {α : Type w} {m : Type (max u w) → Type u_1} {σ : Type (max u w)} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Except ε α)

Execute an EStateT on initial state init to get an Except result, discarding the final state.

Equations

• Lake.EStateT.run' init x = Lake.EResult.toExcept <$> x init

@[inline]

def Lake.EStateT.toStateT {m : Type u → Type u_1} {ε σ α : Type u} [Functor m] (x : EStateT ε σ m α) : StateT σ m (Except ε α)

Convert an EStateT to a StateT, returning an Except result.

Equations

• x.toStateT s = Lake.EResult.toProd <$> x s

@[inline]

def Lake.EStateT.toStateT? {m : Type u → Type u_1} {ε σ α : Type u} [Functor m] (x : EStateT ε σ m α) : StateT σ m (Option α)

Convert an EStateT to a StateT, returning an Option result.

Equations

• x.toStateT? s = Lake.EResult.toProd? <$> x s

@[inline]

def Lake.EStateT.run? {σ : Type v} {α : Type w} {m : Type (max v w) → Type u_1} {ε : Type (max v w)} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Option α × σ)

Execute an EStateT on initial state init to get an Option result, discarding the exception contents.

Equations

• Lake.EStateT.run? init x = Lake.EResult.toProd? <$> x init

@[inline]

def Lake.EStateT.run?' {m : Type u → Type u_1} {ε σ α : Type u} [Functor m] (init : σ) (x : EStateT ε σ m α) : m (Option α)

Execute an EStateT on initial state init to get an Option result, discarding the final state.

Equations

• Lake.EStateT.run?' init x = Lake.EResult.result? <$> x init

@[inline]

def Lake.EStateT.catchExceptions {m : Type u → Type u_1} {ε σ α : Type u} [Monad m] (x : EStateT ε σ m α) (h : ε → StateT σ m α) : StateT σ m α

Equations

• x.catchExceptions h s = do let __do_lift ← x s match __do_lift with | Lake.EResult.ok a s => pure (a, s) | Lake.EResult.error e s => h e s

@[inline]

def Lake.EStateT.lift {m : Type u → Type u_1} {ε σ α : Type u} [Monad m] (x : m α) : EStateT ε σ m α

Lift the m monad into the EStateT ε σ m monad transformer.

Equations

• Lake.EStateT.lift x s = do let a ← x pure (Lake.EResult.ok a s)

instance Lake.EStateT.instMonadLiftOfMonad {m : Type u → Type u_1} {ε σ : Type u} [Monad m] : MonadLift m (EStateT ε σ m)

Equations

• Lake.EStateT.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.25} => Lake.EStateT.lift }

@[inline]

def Lake.EStateT.pure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (a : α) : EStateT ε σ m α

The pure operation of the EStateT monad transformer.

Equations

• Lake.EStateT.pure a s = pure (Lake.EResult.ok a s)

instance Lake.EStateT.instPure {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Pure m] : Pure (EStateT ε σ m)

Equations

• Lake.EStateT.instPure = { pure := fun {α : Type ?u.25} => Lake.EStateT.pure }

@[inline]

def Lake.EStateT.map {ε : Type u} {σ : Type v} {α β : Type w} {m : Type (max (max u v) w) → Type u_1} [Functor m] (f : α → β) (x : EStateT ε σ m α) : EStateT ε σ m β

The map operation of the EStateT monad transformer.

Equations

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

instance Lake.EStateT.instFunctor {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Functor m] : Functor (EStateT ε σ m)

Equations

• Lake.EStateT.instFunctor = { map := fun {α β : Type ?u.30} => Lake.EStateT.map }

@[inline]

def Lake.EStateT.bind {ε : Type u} {σ : Type v} {α β : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : EStateT ε σ m α) (f : α → EStateT ε σ m β) : EStateT ε σ m β

The bind operation of the EStateT monad transformer.

Equations

• x.bind f s = do let __do_lift ← x s match __do_lift with | Lake.EResult.ok a s => f a s | Lake.EResult.error e s => pure (Lake.EResult.error e s)

@[inline]

def Lake.EStateT.seqRight {ε : Type u} {σ : Type v} {α β : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : EStateT ε σ m α) (y : Unit → EStateT ε σ m β) : EStateT ε σ m β

The seqRight operation of the EStateT monad transformer.

Equations

• x.seqRight y s = do let __do_lift ← x s match __do_lift with | Lake.EResult.ok a s => y () s | Lake.EResult.error e s => pure (Lake.EResult.error e s)

@[always_inline]

instance Lake.EStateT.instMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] : Monad (EStateT ε σ m)

Equations

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

@[inline]

def Lake.EStateT.set {ε : Type u} {σ : Type v} {m : Type (max (max u v) w) → Type u_1} [Pure m] (s : σ) : EStateT ε σ m PUnit

The set operation of the EStateT monad.

Equations

• Lake.EStateT.set s x✝ = pure (Lake.EResult.ok PUnit.unit s)

@[inline]

def Lake.EStateT.get {ε : Type u} {σ : Type v} {m : Type (max u v) → Type u_1} [Pure m] : EStateT ε σ m σ

The get operation of the EStateT monad.

Equations

• Lake.EStateT.get s = pure (Lake.EResult.ok s s)

@[inline]

def Lake.EStateT.modifyGet {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (f : σ → α × σ) : EStateT ε σ m α

The modifyGet operation of the EStateT monad transformer.

Equations

• Lake.EStateT.modifyGet f s = match f s with | (a, s) => pure (Lake.EResult.ok a s)

instance Lake.EStateT.instMonadStateOfOfPure {ε : Type u} {σ : Type v} {m : Type (max u v) → Type u_1} [Pure m] : MonadStateOf σ (EStateT ε σ m)

Equations

• Lake.EStateT.instMonadStateOfOfPure = { get := Lake.EStateT.get, set := Lake.EStateT.set, modifyGet := fun {α : Type ?u.25} => Lake.EStateT.modifyGet }

@[inline]

def Lake.EStateT.throw {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (e : ε) : EStateT ε σ m α

The throw operation of the EStateT monad transformer.

Equations

• Lake.EStateT.throw e s = pure (Lake.EResult.error e s)

@[inline]

def Lake.EStateT.tryCatch {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : EStateT ε σ m α) (handle : ε → EStateT ε σ m α) : EStateT ε σ m α

Equations

• x.tryCatch handle s = do let __do_lift ← x s match __do_lift with | Lake.EResult.error e s => handle e s | ok => pure ok

instance Lake.EStateT.instMonadExceptOfOfMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] : MonadExceptOf ε (EStateT ε σ m)

Equations

• Lake.EStateT.instMonadExceptOfOfMonad = { throw := fun {α : Type ?u.26} => Lake.EStateT.throw, tryCatch := fun {α : Type ?u.26} => Lake.EStateT.tryCatch }

@[inline]

def Lake.EStateT.orElse {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x₁ : EStateT ε σ m α) (x₂ : Unit → EStateT ε σ m α) : EStateT ε σ m α

Equations

• x₁.orElse x₂ s = do let __do_lift ← x₁ s match __do_lift with | Lake.EResult.error a s => x₂ () s | ok => pure ok

instance Lake.EStateT.instOrElseOfMonad {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] : OrElse (EStateT ε σ m α)

Equations

• Lake.EStateT.instOrElseOfMonad = { orElse := Lake.EStateT.orElse }

@[inline]

def Lake.EStateT.adaptExcept {ε ε' : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Functor m] (f : ε → ε') (x : EStateT ε σ m α) : EStateT ε' σ m α

Map the exception type of a EStateT ε σ m α by a function f : ε → ε'.

Equations

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

@[always_inline]

instance Lake.EStateT.instMonadFinallyOfMonad {ε : Type u} {σ : Type v} {m : Type (max (max u v) u_1) → Type u_2} [Monad m] : MonadFinally (EStateT ε σ m)

Equations

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

def Lake.EStateT.ofEStateM {ε σ α : Type u_1} (f : EStateM ε σ α) : EStateT ε σ Id α

EStateM is analogous to Lake.EStateT with m := Id.

Equations

• Lake.EStateT.ofEStateM f s = pure (Lake.EResult.ofEStateMResult (f s))

def Lake.EStateT.toEStateM {ε σ α : Type u_1} (f : EStateT ε σ Id α) : EStateM ε σ α

Lake.EStateT with m := Id and all the types in the same universe is analogous to EStateM.

Equations

• f.toEStateM s = (f s).run.toEStateMResult