structure Aesop.ForwardIndex : Type

Index for forward rules.

• tree : Lean.Meta.DiscrTree (ForwardRule × PremiseIndex)

  Maps expressions T to all tuples (r, i) where r : ForwardRule, i : PremiseIndex and the i-th argument of the type of r.expr (counting from zero) likely unifies with T.

• nameToRule : Lean.PHashMap RuleName ForwardRule

  Indexes the forward rules contained in tree by name.

• constRules : Lean.PHashSet ForwardRule

  Constant forward rules, i.e. forward rules that have no premises and no rule pattern.

@[implicit_reducible]

instance Aesop.instInhabitedForwardIndex : Inhabited ForwardIndex

Equations

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

def Aesop.instInhabitedForwardIndex.default : ForwardIndex

Equations

• Aesop.instInhabitedForwardIndex.default = { tree := default, nameToRule := default, constRules := default }

@[implicit_reducible]

instance Aesop.ForwardIndex.instEmptyCollection : EmptyCollection ForwardIndex

Equations

• Aesop.ForwardIndex.instEmptyCollection = { emptyCollection := { tree := { }, nameToRule := { }, constRules := ∅ } }

def Aesop.ForwardIndex.trace (traceOpt : TraceOption) (idx : ForwardIndex) : Lean.CoreM Unit

Trace the rules contained in idx if traceOpt is enabled.

Equations

• One or more equations did not get rendered due to their size.

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

Merge two indices.

Equations

• One or more equations did not get rendered due to their size.

def Aesop.ForwardIndex.insert (r : ForwardRule) (idx : ForwardIndex) : ForwardIndex

Insert a forward rule into the ForwardIndex.

Equations

• One or more equations did not get rendered due to their size.

def Aesop.ForwardIndex.get (idx : ForwardIndex) (e : Lean.Expr) : Lean.MetaM (Array (ForwardRule × PremiseIndex))

Get the forward rules whose maximal premises likely unify with e. Each returned pair (r, i) contains a rule r and the index i of the premise of r that likely unifies with e.

Equations

• idx.get e = Aesop.getUnify idx.tree e

def Aesop.ForwardIndex.getRuleWithName? (n : RuleName) (idx : ForwardIndex) : Option ForwardRule

Get the forward rule with the given rule name.

Equations

• Aesop.ForwardIndex.getRuleWithName? n idx = idx.nameToRule[n]

def Aesop.ForwardIndex.getConstRuleMatches (idx : ForwardIndex) : Array ForwardRuleMatch

Get forward rule matches for the constant forward rules (i.e., those with no premises and no rule pattern). Accordingly, the returned matches contain no hypotheses.

Equations

• idx.getConstRuleMatches = Lean.PersistentHashSet.fold (fun (ms : Array Aesop.ForwardRuleMatch) (r : Aesop.ForwardRule) => ms.push { rule := r, «match» := ∅ }) #[] idx.constRules