Documentation

Lean.Util.MonadCache

@[inline]
def Lean.checkCache {α : Type} {β : Type} {m : TypeType} [inst : Lean.MonadCache α β m] [inst : Monad m] (a : α) (f : Unitm β) :
m β
Equations
instance Lean.instMonadCacheReaderT {α : Type} {β : Type} {ρ : Type} {m : TypeType} [inst : Lean.MonadCache α β m] :
Equations
instance Lean.instMonadCacheExceptT {α : Type} {β : Type} {ε : Type} {m : TypeType} [inst : Lean.MonadCache α β m] [inst : Monad m] :
Equations
@[inline]
def Lean.MonadHashMapCacheAdapter.findCached? {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Lean.MonadHashMapCacheAdapter α β m] (a : α) :
m (Option β)
Equations
@[inline]
def Lean.MonadHashMapCacheAdapter.cache {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Lean.MonadHashMapCacheAdapter α β m] (a : α) (b : β) :
Equations
instance Lean.MonadHashMapCacheAdapter.instMonadCache {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Lean.MonadHashMapCacheAdapter α β m] :
Equations
  • Lean.MonadHashMapCacheAdapter.instMonadCache = { findCached? := Lean.MonadHashMapCacheAdapter.findCached?, cache := Lean.MonadHashMapCacheAdapter.cache }
noncomputable def Lean.MonadCacheT {ω : outParam Type} (α : Type) (β : Type) (m : TypeType) [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] (α : Type) :
Type
Equations
instance Lean.MonadCacheT.instMonadHashMapCacheAdapterMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : MonadLiftT (ST ω) m] [inst : Monad m] :
Equations
  • Lean.MonadCacheT.instMonadHashMapCacheAdapterMonadCacheT = { getCache := get, modifyCache := fun f => modify f }
@[inline]
def Lean.MonadCacheT.run {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : MonadLiftT (ST ω) m] [inst : Monad m] {σ : Type} (x : Lean.MonadCacheT α β m σ) :
m σ
Equations
instance Lean.MonadCacheT.instMonadMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : Monad m] :
Equations
instance Lean.MonadCacheT.instMonadLiftMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] :
Equations
instance Lean.MonadCacheT.instMonadExceptOfMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] (ε : Type u_1) [inst : MonadExceptOf ε m] :
Equations
instance Lean.MonadCacheT.instMonadControlMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] :
Equations
instance Lean.MonadCacheT.instMonadFinallyMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : MonadFinally m] :
Equations
instance Lean.MonadCacheT.instMonadRefMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Lean.MonadRef m] :
Equations
instance Lean.MonadCacheT.instAlternativeMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Alternative m] :
Equations
noncomputable def Lean.MonadStateCacheT (α : Type) (β : Type) (m : TypeType) [inst : BEq α] [inst : Hashable α] (α : Type) :
Type
Equations
instance Lean.MonadStateCacheT.instMonadHashMapCacheAdapterMonadStateCacheT {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] :
Equations
  • Lean.MonadStateCacheT.instMonadHashMapCacheAdapterMonadStateCacheT = { getCache := get, modifyCache := fun f => modify f }
@[inline]
def Lean.MonadStateCacheT.run {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] {σ : Type} (x : Lean.MonadStateCacheT α β m σ) :
m σ
Equations
instance Lean.MonadStateCacheT.instMonadMonadStateCacheT {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] :
Equations
instance Lean.MonadStateCacheT.instMonadLiftMonadStateCacheT {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] :
Equations
instance Lean.MonadStateCacheT.instMonadExceptOfMonadStateCacheT {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] (ε : Type u_1) [inst : MonadExceptOf ε m] :
Equations
instance Lean.MonadStateCacheT.instMonadControlMonadStateCacheT {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] :
Equations
instance Lean.MonadStateCacheT.instMonadFinallyMonadStateCacheT {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : MonadFinally m] :
Equations
instance Lean.MonadStateCacheT.instMonadRefMonadStateCacheT {α : Type} {β : Type} {m : TypeType} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Lean.MonadRef m] :
Equations