@[inline, reducible]

abbrev Lake.CallStack (κ : Type u_1) : Type u_1

A sequence of calls donated by the key type κ.

Equations

• Lake.CallStack κ = List κ

@[inline, reducible]

abbrev Lake.Cycle (κ : Type u_1) : Type u_1

A CallStack ending in a cycle.

Equations

• Lake.Cycle κ = Lake.CallStack κ

@[inline, reducible]

abbrev Lake.CycleT (κ : Type u_1) (m : Type u_1 → Type u_2) (α : Type u_1) : Type (max u_1 u_2)

A transformer that equips a monad with a CallStack to detect cycles.

Equations

• Lake.CycleT κ m = ReaderT (Lake.CallStack κ) (ExceptT (Lake.Cycle κ) m)

@[inline]

def Lake.guardCycle {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [BEq κ] [Monad m] (key : κ) (act : Lake.CycleT κ m α) : Lake.CycleT κ m α

Add key to the monad's CallStack before invoking act. If adding key produces a cycle, the cyclic call stack is thrown.

Equations

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