Documentation

Init.ShareCommon

@[reducible, inline]
Equations
Instances For
    Equations
    Instances For
      @[reducible, inline]
      Equations
      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
            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

              @[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_1} => 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