← Mathematical handbook

def Aesop.RulePatternCache.Entry : Type

Entry of the rule pattern cache.

Equations

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

structure Aesop.RulePatternCache : Type

A cache for the rule pattern index.

• map : Std.HashMap Lean.Expr Entry

@[instance_reducible]

instance Aesop.instInhabitedRulePatternCache : Inhabited RulePatternCache

Equations

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

@[instance_reducible]

instance Aesop.instEmptyCollectionRulePatternCache : EmptyCollection RulePatternCache

Equations

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