Documentation

Lean.Util.ShareCommon

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[inline, reducible]
      abbrev Lean.ShareCommon.ShareCommonT (m : Type u_1 → Type u_2) (α : Type u_1) :
      Type (max u_1 u_2)
      Equations
      Instances For
        @[inline, reducible]
        abbrev Lean.ShareCommon.PShareCommonT (m : Type u_1 → Type u_2) (α : Type u_1) :
        Type (max u_1 u_2)
        Equations
        Instances For
          @[inline, reducible]
          abbrev Lean.ShareCommon.ShareCommonM (α : Type u_1) :
          Type u_1
          Equations
          Instances For
            Equations
            • Lean.ShareCommon.ShareCommonT.monadShareCommon = { withShareCommon := fun {α} => Lean.ShareCommon.ShareCommonT.withShareCommon }
            Equations
            • Lean.ShareCommon.PShareCommonT.monadShareCommon = { withShareCommon := fun {α} => Lean.ShareCommon.PShareCommonT.withShareCommon }
            @[inline]
            def Lean.ShareCommon.ShareCommonT.run {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] :
            Equations
            • Lean.ShareCommon.ShareCommonT.run = ShareCommonT.run
            Instances For
              @[inline]
              def Lean.ShareCommon.PShareCommonT.run {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] :
              Equations
              • Lean.ShareCommon.PShareCommonT.run = ShareCommonT.run
              Instances For
                @[inline]
                Equations
                • Lean.ShareCommon.ShareCommonM.run = Lean.ShareCommon.ShareCommonT.run
                Instances For
                  @[inline]
                  Equations
                  • Lean.ShareCommon.PShareCommonM.run = Lean.ShareCommon.PShareCommonT.run
                  Instances For