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)

def Aesop.preprocessRule : SafeRule

Equations

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

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.

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.