Documentation

Lake.Util.Cycle

@[inline, reducible]
abbrev Lake.CallStack (κ : Type u_1) :
Type u_1

A sequence of calls donated by the key type κ.

Equations
Instances For
    @[inline, reducible]
    abbrev Lake.Cycle (κ : Type u_1) :
    Type u_1

    A CallStack ending in a cycle.

    Equations
    Instances For
      @[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
      Instances For
        @[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.
        Instances For