Documentation

Lake.Config.Context

structure Lake.Context :

A Lake configuration.

Instances For
    @[inline, reducible]
    abbrev Lake.LakeT (m : TypeType u_1) (α : Type) :
    Type u_1

    A transformer to equip a monad with a Lake.Context.

    Equations
    Instances For
      @[inline]
      def Lake.LakeT.run {m : TypeType u_1} {α : Type} (ctx : Lake.Context) (self : Lake.LakeT m α) :
      m α
      Equations
      Instances For
        @[inline, reducible]
        abbrev Lake.LakeM (α : Type) :

        A monad equipped with a Lake.Context.

        Equations
        Instances For
          @[inline]
          def Lake.LakeM.run {α : Type} (ctx : Lake.Context) (self : Lake.LakeM α) :
          α
          Equations
          Instances For