Documentation

Init.ShareCommon

@[reducible, inline]
Equations
    Instances For
      Equations
        Instances For
          @[reducible, inline]
          Equations
            Instances For
              Instances For
                @[reducible, inline]
                Equations
                  Instances For
                    @[extern lean_sharecommon_eq]
                    unsafe opaque ShareCommon.Object.eq (a b : Object) :
                    @[extern lean_sharecommon_hash]
                    Instances For
                      @[implemented_by ShareCommon.StateFactory.mkImpl]

                      Internally State is implemented as a pair ObjectMap and ObjectSet

                      @[reducible, inline]
                      Equations
                        Instances For
                          Equations
                            Instances For
                              @[implemented_by ShareCommon.mkStateImpl]
                              @[extern lean_state_sharecommon]
                              def ShareCommon.State.shareCommon {α : Type u_1} {σ : StateFactory} (s : State σ) (a : α) :
                              α × State σ
                              Equations
                                Instances For
                                  class MonadShareCommon (m : Type u → Type v) :
                                  Type (max (u + 1) v)
                                  • withShareCommon {α : Type u} : αm α
                                  Instances
                                    @[reducible, inline]
                                    abbrev withShareCommon {m : Type u_1 → Type u_2} [self : MonadShareCommon m] {α : Type u_1} :
                                    αm α
                                    Equations
                                      Instances For
                                        @[reducible, inline]
                                        abbrev shareCommonM {m : Type u_1 → Type u_2} {α : Type u_1} [MonadShareCommon m] (a : α) :
                                        m α
                                        Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev ShareCommonT (σ : ShareCommon.StateFactory) (m : Type u → Type v) (α : Type u) :
                                            Type (max u v)
                                            Equations
                                              Instances For
                                                @[reducible, inline]
                                                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
                                                        @[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
                                                                @[extern lean_sharecommon_quick]
                                                                def ShareCommon.shareCommon' {α : Sort u_1} (a : α) :
                                                                α

                                                                A more restrictive but efficient max sharing primitive.

                                                                Remark: it optimizes the number of RC operations, and the strategy for caching results.

                                                                Equations
                                                                  Instances For