Lean.Util.ShareCommon

Instances For

source

def Lean.ShareCommon.persistentObjectFactory :

ShareCommon.StateFactory

Equations

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

Instances For

source

@[reducible, inline]

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

Type (max u_1 u_2)

Instances For

source

@[reducible, inline]

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

Type (max u_1 u_2)

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[specialize #[]]

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

Lean.ShareCommon.ShareCommonT m α

Equations

Lean.ShareCommon.ShareCommonT.withShareCommon a = modifyGet fun (s : ShareCommon.State Lean.ShareCommon.objectFactory) => s.shareCommon a

Instances For

source

@[specialize #[]]

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

Lean.ShareCommon.PShareCommonT m α

Instances For

source

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

MonadShareCommon (Lean.ShareCommon.ShareCommonT m)

Equations

Lean.ShareCommon.ShareCommonT.monadShareCommon = { withShareCommon := fun {α : Type ?u.20} => Lean.ShareCommon.ShareCommonT.withShareCommon }

source

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

MonadShareCommon (Lean.ShareCommon.PShareCommonT m)

source

@[inline]

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

Lean.ShareCommon.ShareCommonT m α → m α

Instances For

source

@[inline]

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

Lean.ShareCommon.PShareCommonT m α → m α

Instances For

source

@[inline]

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

Lean.ShareCommon.ShareCommonM α → α

Instances For

source

@[inline]

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

Lean.ShareCommon.PShareCommonM α → α

Equations

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

Instances For

source

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

Instances For