Lean.Util.ShareCommon

Equations

Instances For

source

def Lean.ShareCommon.persistentObjectFactory :

ShareCommon.StateFactory

Equations

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)

Equations

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)

Equations

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

Instances For

source

@[specialize #[]]

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

ShareCommonT m α

Equations

Instances For

source

@[specialize #[]]

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

PShareCommonT m α

Equations

Instances For

source

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

MonadShareCommon (ShareCommonT m)

Equations

source

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

MonadShareCommon (PShareCommonT m)

Equations

source

@[inline]

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

ShareCommonT m α → m α

Equations

Instances For

source

@[inline]

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

PShareCommonT m α → m α

Equations

Instances For

source

@[inline]

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

ShareCommonM α → α

Equations

Instances For

source

@[inline]

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

PShareCommonM α → α

Equations

Instances For

source

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

Equations

Instances For