@[reducible, inline]

abbrev Aesop.RulePatternSubstMap : Type

A map from rule names to rule pattern substitutions. When run on a goal, the rule pattern index returns such a map.

def Aesop.RulePatternSubstMap.insertArray (xs : Array (RuleName × Substitution)) (m : RulePatternSubstMap) : RulePatternSubstMap

Insert an array of rule pattern substitutions into a rule pattern substitution map.

def Aesop.RulePatternSubstMap.ofArray (xs : Array (RuleName × Substitution)) : RulePatternSubstMap

Build a rule pattern substitution map from an array of substitutions.

def Aesop.RulePatternSubstMap.toFlatArray (m : RulePatternSubstMap) : Array (RuleName × Substitution)

Convert a rule pattern substitution map to a flat array of substitutions.

structure Aesop.RulePatternIndex.Entry : Type

An entry of the rule pattern index.

• name : RuleName

  The name of the rule to which the pattern belongs.

• pattern : RulePattern

  The rule's pattern. We assume that there is at most one pattern per rule.

def Aesop.RulePatternIndex.instInhabitedEntry.default : Entry

@[implicit_reducible]

instance Aesop.RulePatternIndex.instInhabitedEntry : Inhabited Entry

@[implicit_reducible]

instance Aesop.instBEqEntry : BEq RulePatternIndex.Entry

structure Aesop.RulePatternIndex : Type

A rule pattern index. Maps expressions e to rule patterns that likely unify with e.

• tree : Lean.Meta.DiscrTree Entry

  The index.

• isEmpty : Bool

  true iff the index contains no patterns.

def Aesop.instInhabitedRulePatternIndex.default : RulePatternIndex

@[implicit_reducible]

instance Aesop.instInhabitedRulePatternIndex : Inhabited RulePatternIndex

@[implicit_reducible]

instance Aesop.RulePatternIndex.instEmptyCollection : EmptyCollection RulePatternIndex

def Aesop.RulePatternIndex.add (name : RuleName) (pattern : RulePattern) (idx : RulePatternIndex) : RulePatternIndex

Add a rule pattern to the index.

def Aesop.RulePatternIndex.merge (idx₁ idx₂ : RulePatternIndex) : RulePatternIndex

Merge two rule pattern indices. Patterns that appear in both indices appear twice in the result.

def Aesop.RulePatternIndex.getSingle (e : Lean.Expr) (idx : RulePatternIndex) : BaseM (Array (RuleName × Substitution))

Get rule pattern substitutions for the patterns that match e.

def Aesop.RulePatternIndex.getCore (e : Lean.Expr) (idx : RulePatternIndex) : BaseM (Array (RuleName × Substitution))

Get all substitutions of the rule patterns that match a subexpression of e. Subexpressions containing bound variables are not considered. The returned array may contain duplicates.

def Aesop.RulePatternIndex.get (e : Lean.Expr) (idx : RulePatternIndex) : BaseM RulePatternSubstMap

Get all substitutions of the rule patterns that match a subexpression of e. Subexpressions containing bound variables are not considered. The returned array may contain duplicates.

def Aesop.RulePatternIndex.getInLocalDeclCore (acc : RulePatternSubstMap) (ldecl : Lean.LocalDecl) (idx : RulePatternIndex) : BaseM RulePatternSubstMap

Get all substitutions of the rule patterns that match a subexpression of the given local declaration. Subexpressions containing bound variables are not considered.

def Aesop.RulePatternIndex.getInLocalDecl (ldecl : Lean.LocalDecl) (idx : RulePatternIndex) : BaseM RulePatternSubstMap

Get all substitutions of the rule patterns that match a subexpression of the given local declaration. Subexpressions containing bound variables are not considered.

def Aesop.RulePatternIndex.getInGoal (goal : Lean.MVarId) (idx : RulePatternIndex) : BaseM RulePatternSubstMap

Get all substitutions of the rule patterns that match a subexpression of a hypothesis or the target. Subexpressions containing bound variables are not considered.