Documentation

Init.Control.ExceptCps

The Exception monad transformer using CPS style.

def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) :
Type (max (u + 1) v)
Equations
  • ExceptCpsT ε m α = ((β : Type ?u.27) → (αm β)(εm β)m β)
Instances For
    @[inline]
    def ExceptCpsT.run {m : Type u → Type u_1} {ε : Type u} {α : Type u} [Monad m] (x : ExceptCpsT ε m α) :
    m (Except ε α)
    Equations
    Instances For
      @[inline]
      def ExceptCpsT.runK {m : Type u → Type u_1} {β : Type u} {ε : Type u} {α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : αm β) (error : εm β) :
      m β
      Equations
      • x.runK s ok error = x β ok error
      Instances For
        @[inline]
        def ExceptCpsT.runCatch {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (x : ExceptCpsT α m α) :
        m α
        Equations
        • x.runCatch = x α pure pure
        Instances For
          @[always_inline]
          instance ExceptCpsT.instMonad {ε : Type u_1} {m : Type u_1 → Type u_2} :
          Equations
          • ExceptCpsT.instMonad = Monad.mk
          instance ExceptCpsT.instLawfulMonad {σ : Type u_1} {m : Type u_1 → Type u_2} :
          Equations
          • =
          instance ExceptCpsT.instMonadExceptOf {ε : Type u_1} {m : Type u_1 → Type u_2} :
          Equations
          • One or more equations did not get rendered due to their size.
          @[inline]
          def ExceptCpsT.lift {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} [Monad m] (x : m α) :
          ExceptCpsT ε m α
          Equations
          Instances For
            instance ExceptCpsT.instMonadLiftOfMonad {m : Type u_1 → Type u_2} {σ : Type u_1} [Monad m] :
            Equations
            • ExceptCpsT.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.24} => ExceptCpsT.lift }
            instance ExceptCpsT.instInhabited {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} [Inhabited ε] :
            Equations
            • ExceptCpsT.instInhabited = { default := fun (x : Type ?u.32) (x_1 : αm x) (k₂ : εm x) => k₂ default }
            @[simp]
            theorem ExceptCpsT.run_pure {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {x : α} [Monad m] :
            (pure x).run = pure (Except.ok x)
            @[simp]
            theorem ExceptCpsT.run_lift {m : Type u → Type u_1} {α : Type u} {ε : Type u} [Monad m] (x : m α) :
            (ExceptCpsT.lift x).run = do let ax pure (Except.ok a)
            @[simp]
            theorem ExceptCpsT.run_throw {m : Type u_1 → Type u_2} {ε : Type u_1} {β : Type u_1} {e : ε} [Monad m] :
            (throw e).run = pure (Except.error e)
            @[simp]
            theorem ExceptCpsT.run_bind_lift {m : Type u_1 → Type u_2} {α : Type u_1} {ε : Type u_1} {β : Type u_1} [Monad m] (x : m α) (f : αExceptCpsT ε m β) :
            (ExceptCpsT.lift x >>= f).run = do let ax (f a).run
            @[simp]
            theorem ExceptCpsT.run_bind_throw {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] (e : ε) (f : αExceptCpsT ε m β) :
            (throw e >>= f).run = (throw e).run
            @[simp]
            theorem ExceptCpsT.runCatch_pure {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [Monad m] :
            (pure x).runCatch = pure x
            @[simp]
            theorem ExceptCpsT.runCatch_lift {m : Type u → Type u_1} {α : Type u} [Monad m] [LawfulMonad m] (x : m α) :
            (ExceptCpsT.lift x).runCatch = x
            @[simp]
            theorem ExceptCpsT.runCatch_throw {m : Type u_1 → Type u_2} {α : Type u_1} {a : α} [Monad m] :
            (throw a).runCatch = pure a
            @[simp]
            theorem ExceptCpsT.runCatch_bind_lift {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [Monad m] (x : m α) (f : αExceptCpsT β m β) :
            (ExceptCpsT.lift x >>= f).runCatch = do let ax (f a).runCatch
            @[simp]
            theorem ExceptCpsT.runCatch_bind_throw {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_1} [Monad m] (e : β) (f : αExceptCpsT β m β) :
            (throw e >>= f).runCatch = pure e