Documentation
Aesop
.
RulePattern
.
Cache
Search
return to top
source
Imports
Init
Aesop.Forward.Substitution
Aesop.Rule.Name
Imported by
Aesop
.
RulePatternCache
.
Entry
Aesop
.
RulePatternCache
Aesop
.
instInhabitedRulePatternCache
Aesop
.
instEmptyCollectionRulePatternCache
source
def
Aesop
.
RulePatternCache
.
Entry
:
Type
Entry of the rule pattern cache.
Equations
Aesop.RulePatternCache.Entry
=
Array
(
Aesop.RuleName
×
Aesop.Substitution
)
Instances For
source
structure
Aesop
.
RulePatternCache
:
Type
A cache for the rule pattern index.
map :
Std.HashMap
Lean.Expr
Entry
Instances For
source
instance
Aesop
.
instInhabitedRulePatternCache
:
Inhabited
RulePatternCache
Equations
Aesop.instInhabitedRulePatternCache
=
{
default
:=
{
map
:=
default
}
}
source
instance
Aesop
.
instEmptyCollectionRulePatternCache
:
EmptyCollection
RulePatternCache
Equations
Aesop.instEmptyCollectionRulePatternCache
=
{
emptyCollection
:=
{
map
:=
∅
}
}