def Aesop.RulePatternCache.Entry : Type

Entry of the rule pattern cache.

Equations

• Aesop.RulePatternCache.Entry = Array (Aesop.RuleName × Aesop.Substitution)

Instances For

• Aesop.BaseM.instMonadHashMapCacheAdapterExprEntry

structure Aesop.RulePatternCache : Type

A cache for the rule pattern index.

• map : Std.HashMap Lean.Expr Entry

Instances For

• Aesop.instEmptyCollectionRulePatternCache
• Aesop.instInhabitedRulePatternCache

instance Aesop.instInhabitedRulePatternCache : Inhabited RulePatternCache

Equations

• Aesop.instInhabitedRulePatternCache = { default := { map := default } }

instance Aesop.instEmptyCollectionRulePatternCache : EmptyCollection RulePatternCache

Equations

• Aesop.instEmptyCollectionRulePatternCache = { emptyCollection := { map := ∅ } }