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.

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

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

• error: {ε : Type u} → {σ : Type v} → {α : Type w} → ε → σ → Lake.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 (Lake.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 (Lake.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} : Lake.EResult ε σ α → σ

Extract the state σ from a EResult ε σ α.

Equations

• x.state = match x with | Lake.EResult.ok a s => s | Lake.EResult.error a s => s

@[inline]

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

Equations

• Lake.EResult.setState s x = match x with | Lake.EResult.ok a a_1 => Lake.EResult.ok a s | Lake.EResult.error e a => Lake.EResult.error e s

@[inline]

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

Extract the result α from a EResult ε σ α.

Equations

• x.result? = match x with | Lake.EResult.ok a a_1 => some a | x => none

@[inline]

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

Extract the error ε from a EResult ε σ α.

Equations

• x.error? = match x with | Lake.EResult.error e a => some e | x => none

@[inline]

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

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

Equations

• x.toExcept = match x with | Lake.EResult.ok a a_1 => Except.ok a | Lake.EResult.error e a => Except.error e

@[inline]

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

Equations

• Lake.EResult.map f x = match x with | Lake.EResult.ok a s => Lake.EResult.ok (f a) s | Lake.EResult.error e s => Lake.EResult.error e s

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

Equations

• Lake.instFunctorEResult = { map := fun {α β : Type u_3} => Lake.EResult.map, mapConst := fun {α β : Type u_3} => Lake.EResult.map ∘ Function.const β }

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_1} {m : Type (max (max u_2 u_3) u_1) → Type u_4} {σ : Type u_3} {α : Type u_2} [Inhabited ε] [Pure m] : Inhabited (Lake.EStateT ε σ m α)

Equations

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

@[inline]

def Lake.EStateT.lift {m : Type u → Type u_1} {ε : Type u} {σ : Type u} {α : Type u} [Monad m] (x : m α) : Lake.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 (max (max u_1 (max u_2 u_1) u_3) (max (max u_2 u_1) u_3) u_1) → Type u_4} {ε : Type (max (max (max u_2 u_1) u_3) u_1)} {σ : Type (max (max u_2 u_1) u_3)} [Monad m] : MonadLift m (Lake.EStateT ε σ m)

Equations

• Lake.EStateT.instMonadLiftOfMonad = { monadLift := fun {α : Type (max (max (max u_2 u_1) u_3) u_1)} => Lake.EStateT.lift }

@[inline]

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

Execute an EStateT on initial state s 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 : σ) (self : Lake.EStateT ε σ m α) : m (Except ε α)

Execute an EStateT on initial state s to get an Except result.

Equations

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

@[inline]

def Lake.EStateT.pure {ε : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Pure m] (a : α) : Lake.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 (Lake.EStateT ε σ m)

Equations

• Lake.EStateT.instPure = { pure := fun {α : Type u_1} => Lake.EStateT.pure }

@[inline]

def Lake.EStateT.map {ε : Type u} {σ : Type v} {α : Type w} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [Functor m] (f : α → β) (x : Lake.EStateT ε σ m α) : Lake.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 (Lake.EStateT ε σ m)

Equations

• Lake.EStateT.instFunctor = { map := fun {α β : Type u_1} => Lake.EStateT.map, mapConst := fun {α β : Type u_1} => Lake.EStateT.map ∘ Function.const β }

@[inline]

def Lake.EStateT.bind {ε : Type u} {σ : Type v} {α : Type w} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : Lake.EStateT ε σ m α) (f : α → Lake.EStateT ε σ m β) : Lake.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} {β : Type w} {m : Type (max (max u v) w) → Type u_1} [Monad m] (x : Lake.EStateT ε σ m α) (y : Unit → Lake.EStateT ε σ m β) : Lake.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 (Lake.EStateT ε σ m)

Equations

• Lake.EStateT.instMonad = Monad.mk

@[inline]

def Lake.EStateT.set {ε : Type u} {σ : Type v} {m : Type (max (max u v) w) → Type u_1} [Pure m] (s : σ) : Lake.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] : Lake.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 : σ → α × σ) : Lake.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 σ (Lake.EStateT ε σ m)

Equations

• Lake.EStateT.instMonadStateOfOfPure = { get := Lake.EStateT.get, set := Lake.EStateT.set, modifyGet := fun {α : Type v} => 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 : ε) : Lake.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 : Lake.EStateT ε σ m α) (handle : ε → Lake.EStateT ε σ m α) : Lake.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 ε (Lake.EStateT ε σ m)

Equations

• Lake.EStateT.instMonadExceptOfOfMonad = { throw := fun {α : Type u_1} => Lake.EStateT.throw, tryCatch := fun {α : Type u_1} => 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₁ : Lake.EStateT ε σ m α) (x₂ : Unit → Lake.EStateT ε σ m α) : Lake.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 (Lake.EStateT ε σ m α)

Equations

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

@[inline]

def Lake.EStateT.adaptExcept {ε : Type u} {ε' : Type u} {σ : Type v} {α : Type w} {m : Type (max (max u v) w) → Type u_1} [Functor m] (f : ε → ε') (x : Lake.EStateT ε σ m α) : Lake.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 (Lake.EStateT ε σ m)

Equations

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