Documentation

Init.ShareCommon

@[inline, reducible]
Equations
Instances For
    @[inline, reducible]
    Equations
    Instances For
      Instances For
        @[extern lean_sharecommon_eq]
        @[extern lean_sharecommon_hash]
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[implemented_by ShareCommon.StateFactory.mkImpl]

            Internally State is implemented as a pair ObjectMap and ObjectSet

            @[implemented_by ShareCommon.mkStateImpl]
            Equations
            @[extern lean_state_sharecommon]
            Equations
            Instances For
              class MonadShareCommon (m : Type u → Type v) :
              Type (max (u + 1) v)
              • withShareCommon : {α : Type u} → αm α
              Instances
                @[inline, reducible]
                abbrev withShareCommon {m : Type u_1 → Type u_2} [self : MonadShareCommon m] {α : Type u_1} :
                αm α
                Equations
                Instances For
                  @[inline, reducible]
                  abbrev shareCommonM {m : Type u_1 → Type u_2} {α : Type u_1} [MonadShareCommon m] (a : α) :
                  m α
                  Equations
                  Instances For
                    @[inline, reducible]
                    abbrev ShareCommonT (σ : ShareCommon.StateFactory) (m : Type u → Type v) (α : Type u) :
                    Type (max u v)
                    Equations
                    Instances For
                      @[inline, reducible]
                      abbrev ShareCommonM (σ : ShareCommon.StateFactory) (α : Type u_1) :
                      Type u_1
                      Equations
                      Instances For
                        @[specialize #[]]
                        def ShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} {σ : ShareCommon.StateFactory} [Monad m] (a : α) :
                        ShareCommonT σ m α
                        Equations
                        Instances For
                          Equations
                          • ShareCommonT.monadShareCommon = { withShareCommon := fun {α} => ShareCommonT.withShareCommon }
                          @[inline]
                          def ShareCommonT.run {m : Type u_1 → Type u_2} {σ : ShareCommon.StateFactory} {α : Type u_1} [Monad m] (x : ShareCommonT σ m α) :
                          m α
                          Equations
                          Instances For
                            @[inline]
                            def ShareCommonM.run {σ : ShareCommon.StateFactory} {α : Type u_1} (x : ShareCommonM σ α) :
                            α
                            Equations
                            Instances For