def Aesop.selectNormRules {m : Type → Type} [Monad m] [Aesop.MonadStats m] [MonadLiftT Lean.MetaM m] (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) : m (Array (Aesop.IndexMatchResult Aesop.NormRule))

Equations

• Aesop.selectNormRules rs goal = Aesop.profilingRuleSelection (liftM (Aesop.LocalRuleSet.applicableNormalizationRules rs goal))

def Aesop.preprocessRule : 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

• 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

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