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

Equations

• Aesop.selectNormRules rs goal = Aesop.profilingRuleSelection (liftM (rs.applicableNormalizationRules 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.