class Lean.MonadCache (α : Type) (β : Type) (m : Type → Type) : Type

• findCached? : α → m (Option β)
• cache : α → β → m Unit

Interface for caching results.

@[inline]

def Lean.checkCache {α : Type} {β : Type} {m : Type → Type} [Lean.MonadCache α β m] [Monad m] (a : α) (f : Unit → m β) : m β

If entry a := b is already in the cache, then return b. Otherwise, execute b ← f (), store a := b in the cache and return b.

instance Lean.instMonadCacheReaderT {α : Type} {β : Type} {ρ : Type} {m : Type → Type} [Lean.MonadCache α β m] : Lean.MonadCache α β (ReaderT ρ m)

@[always_inline]

instance Lean.instMonadCacheExceptT {α : Type} {β : Type} {ε : Type} {m : Type → Type} [Lean.MonadCache α β m] [Monad m] : Lean.MonadCache α β (ExceptT ε m)

class Lean.MonadHashMapCacheAdapter (α : Type) (β : Type) (m : Type → Type) [BEq α] [Hashable α] : Type

• getCache : m (Lean.HashMap α β)
• modifyCache : (Lean.HashMap α β → Lean.HashMap α β) → m Unit

Adapter for implementing MonadCache interface using HashMaps. We just have to specify how to extract/modify the HashMap.

@[inline]

def Lean.MonadHashMapCacheAdapter.findCached? {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [Lean.MonadHashMapCacheAdapter α β m] (a : α) : m (Option β)

@[inline]

def Lean.MonadHashMapCacheAdapter.cache {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Lean.MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit

instance Lean.MonadHashMapCacheAdapter.instMonadCache {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [Lean.MonadHashMapCacheAdapter α β m] : Lean.MonadCache α β m

def Lean.MonadCacheT {ω : Type} (α : Type) (β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [Hashable α] (α : Type) : Type

instance Lean.MonadCacheT.instMonadHashMapCacheAdapterMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] : Lean.MonadHashMapCacheAdapter α β (Lean.MonadCacheT α β m)

@[inline]

def Lean.MonadCacheT.run {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] {σ : Type} (x : Lean.MonadCacheT α β m σ) : m σ

instance Lean.MonadCacheT.instMonadMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [Monad m] : Monad (Lean.MonadCacheT α β m)

instance Lean.MonadCacheT.instMonadLiftMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] : MonadLift m (Lean.MonadCacheT α β m)

instance Lean.MonadCacheT.instMonadExceptOfMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] (ε : Type u_1) [MonadExceptOf ε m] : MonadExceptOf ε (Lean.MonadCacheT α β m)

instance Lean.MonadCacheT.instMonadControlMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] : MonadControl m (Lean.MonadCacheT α β m)

instance Lean.MonadCacheT.instMonadFinallyMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [Monad m] [MonadFinally m] : MonadFinally (Lean.MonadCacheT α β m)

instance Lean.MonadCacheT.instMonadRefMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [Monad m] [Lean.MonadRef m] : Lean.MonadRef (Lean.MonadCacheT α β m)

instance Lean.MonadCacheT.instAlternativeMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [Monad m] [Alternative m] : Alternative (Lean.MonadCacheT α β m)

def Lean.MonadStateCacheT (α : Type) (β : Type) (m : Type → Type) [BEq α] [Hashable α] (α : Type) : Type

instance Lean.MonadStateCacheT.instMonadHashMapCacheAdapterMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] : Lean.MonadHashMapCacheAdapter α β (Lean.MonadStateCacheT α β m)

@[inline]

def Lean.MonadStateCacheT.run {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] {σ : Type} (x : Lean.MonadStateCacheT α β m σ) : m σ

instance Lean.MonadStateCacheT.instMonadMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] : Monad (Lean.MonadStateCacheT α β m)

instance Lean.MonadStateCacheT.instMonadLiftMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] : MonadLift m (Lean.MonadStateCacheT α β m)

instance Lean.MonadStateCacheT.instMonadExceptOfMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] (ε : Type u_1) [MonadExceptOf ε m] : MonadExceptOf ε (Lean.MonadStateCacheT α β m)

instance Lean.MonadStateCacheT.instMonadControlMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] : MonadControl m (Lean.MonadStateCacheT α β m)

instance Lean.MonadStateCacheT.instMonadFinallyMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadFinally m] : MonadFinally (Lean.MonadStateCacheT α β m)

instance Lean.MonadStateCacheT.instMonadRefMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [Lean.MonadRef m] : Lean.MonadRef (Lean.MonadStateCacheT α β m)