Documentation

Init.ShareCommon

@[reducible, inline]
Equations
Instances For
    @[reducible, inline]
    Instances For
      Instances For
        @[extern lean_sharecommon_eq]
        @[extern lean_sharecommon_hash]
        • Map : (α : Type) → Type[inst : BEq α] → [inst : Hashable α] → Type
        • mkMap : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Natself.Map α β
        • mapFind? : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → self.Map α βαOption β
        • mapInsert : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → self.Map α βαβself.Map α β
        • Set : (α : Type) → [inst : BEq α] → [inst : Hashable α] → Type
        • mkSet : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Natself.Set α
        • setFind? : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → self.Set ααOption α
        • setInsert : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → self.Set ααself.Set α
        Instances For
          @[implemented_by ShareCommon.StateFactory.mkImpl]

          Internally State is implemented as a pair ObjectMap and ObjectSet

          @[reducible, inline]
          Equations
          Instances For
            @[implemented_by ShareCommon.mkStateImpl]
            Equations
            @[extern lean_state_sharecommon]
            Equations
            • s.shareCommon a = (a, s)
            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
                          Equations
                          • ShareCommonT.monadShareCommon = { withShareCommon := fun {α : Type ?u.24} => 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
                              @[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