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.

instance Aesop.instInhabitedForwardIndex : Inhabited ForwardIndex

instance Aesop.ForwardIndex.instEmptyCollection : EmptyCollection ForwardIndex

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

Trace the rules contained in idx if traceOpt is enabled.

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

Merge two indices.

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

Insert a forward rule into the ForwardIndex.

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.

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

Get the forward rule with the given rule name.

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.