@[reducible, inline]

abbrev ShareCommon.Object : Type

unsafe def ShareCommon.Object.ptrEq (a b : Object) : Bool

@[reducible, inline]

unsafe abbrev ShareCommon.Object.ptrHash (a : Object) : UInt64

structure ShareCommon.StateFactoryImpl : Type 1

• Map : Type
• Set : Type
• mkState : Unit → self.Map × self.Set
• mapFind? (m : self.Map) (k : Object) : Option Object
• mapInsert (m : self.Map) (k v : Object) : self.Map
• setFind? (m : self.Set) (k : Object) : Option Object
• setInsert (m : self.Set) (o : Object) : self.Set

opaque ShareCommon.StateFactoryPointed : NonemptyType

@[reducible, inline]

abbrev ShareCommon.StateFactory : Type

instance ShareCommon.instNonemptyStateFactory : Nonempty StateFactory

@[extern lean_sharecommon_eq]

unsafe opaque ShareCommon.Object.eq (a b : Object) : Bool

@[extern lean_sharecommon_hash]

unsafe opaque ShareCommon.Object.hash (a : Object) : UInt64

structure ShareCommon.StateFactoryBuilder : Type 1

• Map (α _β : Type) [BEq α] [Hashable α] : Type
• mkMap {α β : Type} [BEq α] [Hashable α] (capacity : Nat) : self.Map α β
• mapFind? {α β : Type} [BEq α] [Hashable α] : self.Map α β → α → Option β
• mapInsert {α β : Type} [BEq α] [Hashable α] : self.Map α β → α → β → self.Map α β
• Set (α : Type) [BEq α] [Hashable α] : Type
• mkSet {α : Type} [BEq α] [Hashable α] (capacity : Nat) : self.Set α
• setFind? {α : Type} [BEq α] [Hashable α] : self.Set α → α → Option α
• setInsert {α : Type} [BEq α] [Hashable α] : self.Set α → α → self.Set α

unsafe def ShareCommon.StateFactory.mkImpl : StateFactoryBuilder → StateFactory

@[implemented_by ShareCommon.StateFactory.mkImpl]

opaque ShareCommon.StateFactory.mk : StateFactoryBuilder → StateFactory

unsafe def ShareCommon.StateFactory.get : StateFactory → StateFactoryImpl

opaque ShareCommon.StatePointed (σ : StateFactory) : NonemptyType

Internally State is implemented as a pair ObjectMap and ObjectSet

@[reducible, inline]

abbrev ShareCommon.State (σ : StateFactory) : Type u

instance ShareCommon.instNonemptyState {σ : StateFactory} : Nonempty (State σ)

unsafe def ShareCommon.mkStateImpl (σ : StateFactory) : State σ

@[implemented_by ShareCommon.mkStateImpl]

opaque ShareCommon.State.mk (σ : StateFactory) : State σ

@[implicit_reducible]

instance ShareCommon.instInhabitedState {σ : StateFactory} : Inhabited (State σ)

@[extern lean_state_sharecommon]

def ShareCommon.State.shareCommon {α : Type u_1} {σ : StateFactory} (s : State σ) (a : α) : α × State σ

class MonadShareCommon (m : Type u → Type v) : Type (max (u + 1) v)

• withShareCommon {α : Type u} : α → m α

@[reducible, inline]

abbrev withShareCommon {m : Type u_1 → Type u_2} [self : MonadShareCommon m] {α : Type u_1} : α → m α

@[reducible, inline]

abbrev shareCommonM {m : Type u_1 → Type u_2} {α : Type u_1} [MonadShareCommon m] (a : α) : m α

@[reducible, inline]

abbrev ShareCommonT (σ : ShareCommon.StateFactory) (m : Type u → Type v) (α : Type u) : Type (max u v)

@[reducible, inline]

abbrev ShareCommonM (σ : ShareCommon.StateFactory) (α : Type u_1) : Type u_1

@[specialize #[]]

def ShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} {σ : ShareCommon.StateFactory} [Monad m] (a : α) : ShareCommonT σ m α

@[implicit_reducible]

instance ShareCommonT.monadShareCommon {m : Type u_1 → Type u_2} {σ : ShareCommon.StateFactory} [Monad m] : MonadShareCommon (ShareCommonT σ m)

@[inline]

def ShareCommonT.run {m : Type u_1 → Type u_2} {σ : ShareCommon.StateFactory} {α : Type u_1} [Monad m] (x : ShareCommonT σ m α) : m α

@[inline]

def ShareCommonM.run {σ : ShareCommon.StateFactory} {α : Type u_1} (x : ShareCommonM σ α) : α

@[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.