@[reducible, inline]
Equations
Instances For
Instances For
Instances For
Equations
Instances For
@[implemented_by ShareCommon.StateFactory.mkImpl]
Equations
Instances For
Internally State
is implemented as a pair ObjectMap
and ObjectSet
@[reducible, inline]
Equations
Instances For
@[implemented_by ShareCommon.mkStateImpl]
@[extern lean_state_sharecommon]
Equations
Instances For
@[reducible, inline]
abbrev
withShareCommon
{m : Type u_1 → Type u_2}
[self : MonadShareCommon m]
{α : Type u_1}
:
α → m α
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
abbrev
ShareCommonT
(σ : ShareCommon.StateFactory)
(m : Type u → Type v)
(α : Type u)
:
Type (max u v)
Equations
Instances For
@[reducible, inline]
Equations
Instances For
@[specialize #[]]
def
ShareCommonT.withShareCommon
{m : Type u_1 → Type u_2}
{α : Type u_1}
{σ : ShareCommon.StateFactory}
[Monad m]
(a : α)
:
ShareCommonT σ m α
Equations
Instances For
instance
ShareCommonT.monadShareCommon
{m : Type u_1 → Type u_2}
{σ : ShareCommon.StateFactory}
[Monad m]
:
MonadShareCommon (ShareCommonT σ m)
Equations
@[inline]
def
ShareCommonT.run
{m : Type u_1 → Type u_2}
{σ : ShareCommon.StateFactory}
{α : Type u_1}
[Monad m]
(x : ShareCommonT σ m α)
:
m α
Equations
Instances For
@[inline]
Equations
Instances For
@[extern lean_sharecommon_quick]
A more restrictive but efficient max sharing primitive.
Remark: it optimizes the number of RC operations, and the strategy for caching results.