@[inline, reducible]

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

A sequence of calls donated by the key type κ.

@[inline, reducible]

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

A CallStack ending in a cycle.

@[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.

@[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.