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))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
def
Aesop.selectUnsafeRules
{Q : Type}
[Queue Q]
(postponedSafeRules : Array PostponedSafeRule)
(gref : GoalRef)
:
Equations
- One or more equations did not get rendered due to their size.