def Lean.ShareCommon.objectFactory : ShareCommon.StateFactory

Equations

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

def Lean.ShareCommon.persistentObjectFactory : ShareCommon.StateFactory

Equations

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

@[inline]

abbrev Lean.ShareCommon.ShareCommonT (m : Type u_1 → Type u_2) (α : Type u_1) : Type (max u_1 u_2)

Equations

• Lean.ShareCommon.ShareCommonT = ShareCommonT Lean.ShareCommon.objectFactory

@[inline]

abbrev Lean.ShareCommon.PShareCommonT (m : Type u_1 → Type u_2) (α : Type u_1) : Type (max u_1 u_2)

Equations

• Lean.ShareCommon.PShareCommonT = ShareCommonT Lean.ShareCommon.persistentObjectFactory

@[inline]

abbrev Lean.ShareCommon.ShareCommonM (α : Type u_1) : Type u_1

Equations

• Lean.ShareCommon.ShareCommonM = Lean.ShareCommon.ShareCommonT Id

@[inline]

abbrev Lean.ShareCommon.PShareCommonM (α : Type u_1) : Type u_1

Equations

• Lean.ShareCommon.PShareCommonM = Lean.ShareCommon.PShareCommonT Id

@[specialize #[]]

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

Equations

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

@[specialize #[]]

def Lean.ShareCommon.PShareCommonT.withShareCommon {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (a : α) : Lean.ShareCommon.PShareCommonT m α

Equations

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

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

Equations

• Lean.ShareCommon.ShareCommonT.monadShareCommon = { withShareCommon := fun {α} => Lean.ShareCommon.ShareCommonT.withShareCommon }

instance Lean.ShareCommon.PShareCommonT.monadShareCommon {m : Type u_1 → Type u_2} [inst : Monad m] : MonadShareCommon (Lean.ShareCommon.PShareCommonT m)

Equations

• Lean.ShareCommon.PShareCommonT.monadShareCommon = { withShareCommon := fun {α} => Lean.ShareCommon.PShareCommonT.withShareCommon }

@[inline]

def Lean.ShareCommon.ShareCommonT.run {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] : Lean.ShareCommon.ShareCommonT m α → m α

Equations

• Lean.ShareCommon.ShareCommonT.run = ShareCommonT.run

@[inline]

def Lean.ShareCommon.PShareCommonT.run {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] : Lean.ShareCommon.PShareCommonT m α → m α

Equations

• Lean.ShareCommon.PShareCommonT.run = ShareCommonT.run

@[inline]

def Lean.ShareCommon.ShareCommonM.run {α : Type u_1} : Lean.ShareCommon.ShareCommonM α → α

Equations

• Lean.ShareCommon.ShareCommonM.run = Lean.ShareCommon.ShareCommonT.run

@[inline]

def Lean.ShareCommon.PShareCommonM.run {α : Type u_1} : Lean.ShareCommon.PShareCommonM α → α

Equations

• Lean.ShareCommon.PShareCommonM.run = Lean.ShareCommon.PShareCommonT.run

def Lean.ShareCommon.shareCommon {α : Type u_1} (a : α) : α

Equations

• Lean.ShareCommon.shareCommon a = Lean.ShareCommon.ShareCommonM.run (withShareCommon a)