def Aesop.selectNormRules (rs : Aesop.RuleSet) (goal : Lean.MVarId) : Aesop.ProfileT Lean.MetaM (Array (Aesop.IndexMatchResult Aesop.NormRule))

Equations

• Aesop.selectNormRules rs goal = Aesop.profiling (liftM (Aesop.RuleSet.applicableNormalizationRules rs goal)) fun x elapsed => Aesop.recordRuleSelectionProfile elapsed

def Aesop.preprocessRule : Aesop.SafeRule

Equations

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

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

Equations

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

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

Equations

• Aesop.selectSafeRules g = Aesop.profiling (Aesop.selectSafeRulesCore g) fun x elapsed => Aesop.recordRuleSelectionProfile elapsed

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

Equations

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

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

Equations

• Aesop.selectUnsafeRules postponedSafeRules gref = Aesop.profiling (Aesop.selectUnsafeRulesCore postponedSafeRules gref) fun x elapsed => Aesop.recordRuleSelectionProfile elapsed