@[inline, reducible]

abbrev ShareCommon.Object : Type

Equations

• ShareCommon.Object = NonScalar

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

Equations

• ShareCommon.Object.ptrEq a b = (ptrAddrUnsafe a == ptrAddrUnsafe b)

@[inline, reducible]

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

Equations

• ShareCommon.Object.ptrHash a = USize.toUInt64 (ptrAddrUnsafe a)

structure ShareCommon.StateFactoryImpl : Type 1

• Map : Type
• Set : Type
• mkState : Unit → s.Map × s.Set
• mapFind? : s.Map → ShareCommon.Object → Option ShareCommon.Object
• mapInsert : s.Map → ShareCommon.Object → ShareCommon.Object → s.Map
• setFind? : s.Set → ShareCommon.Object → Option ShareCommon.Object
• setInsert : s.Set → ShareCommon.Object → s.Set

opaque ShareCommon.StateFactoryPointed : NonemptyType

@[inline, reducible]

abbrev ShareCommon.StateFactory : Type

Equations

• ShareCommon.StateFactory = NonemptyType.type ShareCommon.StateFactoryPointed

instance ShareCommon.instNonemptyStateFactory : Nonempty ShareCommon.StateFactory

Equations

• ShareCommon.instNonemptyStateFactory = ShareCommon.instNonemptyStateFactory.proof_1

@[extern lean_sharecommon_eq]

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

@[extern lean_sharecommon_hash]

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

structure ShareCommon.StateFactoryBuilder : Type 1

• Map : (α : Type) → Type → [inst : BEq α] → [inst : Hashable α] → Type
• mkMap : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Nat → ShareCommon.StateFactoryBuilder.Map s α β
• mapFind? : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ShareCommon.StateFactoryBuilder.Map s α β → α → Option β
• mapInsert : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ShareCommon.StateFactoryBuilder.Map s α β → α → β → ShareCommon.StateFactoryBuilder.Map s α β
• Set : (α : Type) → [inst : BEq α] → [inst : Hashable α] → Type
• mkSet : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Nat → ShareCommon.StateFactoryBuilder.Set s α
• setFind? : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ShareCommon.StateFactoryBuilder.Set s α → α → Option α
• setInsert : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ShareCommon.StateFactoryBuilder.Set s α → α → ShareCommon.StateFactoryBuilder.Set s α

unsafe def ShareCommon.StateFactory.mkImpl : ShareCommon.StateFactoryBuilder → ShareCommon.StateFactory

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by ShareCommon.StateFactory.mkImpl]

opaque ShareCommon.StateFactory.mk : ShareCommon.StateFactoryBuilder → ShareCommon.StateFactory

unsafe def ShareCommon.StateFactory.get : ShareCommon.StateFactory → ShareCommon.StateFactoryImpl

Equations

• ShareCommon.StateFactory.get = unsafeCast

opaque ShareCommon.StatePointed (σ : ShareCommon.StateFactory) : NonemptyType

Internally State is implemented as a pair ObjectMap and ObjectSet

@[inline, reducible]

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

Equations

• ShareCommon.State σ = NonemptyType.type (ShareCommon.StatePointed σ)

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

Equations

• @ShareCommon.instNonemptyState = @ShareCommon.instNonemptyState.proof_1

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

Equations

• ShareCommon.mkStateImpl σ = unsafeCast (ShareCommon.StateFactoryImpl.mkState (ShareCommon.StateFactory.get σ) ())

@[implemented_by ShareCommon.mkStateImpl]

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

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

Equations

• ShareCommon.instInhabitedState = { default := ShareCommon.State.mk σ }

@[extern lean_state_sharecommon]

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

Equations

• ShareCommon.State.shareCommon s a = (a, s)

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

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

@[inline, reducible]

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

Equations

• @withShareCommon = @MonadShareCommon.withShareCommon

@[inline, reducible]

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

Equations

• shareCommonM a = withShareCommon a

@[inline, reducible]

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

Equations

• ShareCommonT σ m = StateT (ShareCommon.State σ) m

@[inline, reducible]

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

Equations

• ShareCommonM σ = ShareCommonT σ Id

@[specialize #[]]

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

Equations

• ShareCommonT.withShareCommon a = modifyGet fun s => ShareCommon.State.shareCommon s a

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

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

• ShareCommonT.run x = StateT.run' x default

@[inline]

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

Equations

• ShareCommonM.run x = ShareCommonT.run x