source
def Aesop.selectNormRules (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) :
BaseM (Array (IndexMatchResult NormRule))
Equations

- Aesop.selectNormRules rs fms goal = Aesop.profilingRuleSelection (rs.applicableNormalizationRules fms goal)

Instances For

source
def Aesop.preprocessRule :
SafeRule
Equations

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

Instances For

source
def Aesop.selectSafeRules {Q : Type} [Queue Q] (g : Goal) :
SearchM Q (Array (IndexMatchResult SafeRule))
Equations

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

Instances For

source
def Aesop.selectUnsafeRules {Q : Type} [Queue Q] (postponedSafeRules : Array PostponedSafeRule) (gref : GoalRef) :
SearchM Q UnsafeQueue
Equations

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

Instances For