Documentation

Lean.Util.ShareCommon

source
def Lean.ShareCommon.objectFactory :
ShareCommon.StateFactory
Instances For
    source
    def Lean.ShareCommon.persistentObjectFactory :
    ShareCommon.StateFactory
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.ShareCommon.ShareCommonT (m : Type u_1 → Type u_2) (α : Type u_1) :
      Type (max u_1 u_2)
      Instances For
        source
        @[reducible, inline]
        abbrev Lean.ShareCommon.PShareCommonT (m : Type u_1 → Type u_2) (α : Type u_1) :
        Type (max u_1 u_2)
        Instances For
          source
          @[reducible, inline]
          abbrev Lean.ShareCommon.ShareCommonM (α : Type u_1) :
          Type u_1
          Instances For
            source
            @[reducible, inline]
            abbrev Lean.ShareCommon.PShareCommonM (α : Type u_1) :
            Type u_1
            Instances For
              source
              @[specialize #[]]
              def Lean.ShareCommon.ShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (a : α) :
              ShareCommonT m α
              Instances For
                source
                @[specialize #[]]
                def Lean.ShareCommon.PShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (a : α) :
                PShareCommonT m α
                Instances For
                  source
                  @[implicit_reducible]
                  instance Lean.ShareCommon.ShareCommonT.monadShareCommon {m : Type u_1 → Type u_2} [Monad m] :
                  MonadShareCommon (ShareCommonT m)
                  source
                  @[implicit_reducible]
                  instance Lean.ShareCommon.PShareCommonT.monadShareCommon {m : Type u_1 → Type u_2} [Monad m] :
                  MonadShareCommon (PShareCommonT m)
                  source
                  @[inline]
                  def Lean.ShareCommon.ShareCommonT.run {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] :
                  ShareCommonT m α → m α
                  Instances For
                    source
                    @[inline]
                    def Lean.ShareCommon.PShareCommonT.run {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] :
                    PShareCommonT m α → m α
                    Instances For
                      source
                      @[inline]
                      def Lean.ShareCommon.ShareCommonM.run {α : Type u_1} :
                      ShareCommonM α → α
                      Instances For
                        source
                        @[inline]
                        def Lean.ShareCommon.PShareCommonM.run {α : Type u_1} :
                        PShareCommonM α → α
                        Instances For
                          source
                          def Lean.ShareCommon.shareCommon {α : Type u_1} (a : α) :
                          α
                          Instances For