def Aesop.PhaseSpec.getSimpPrio {m : Type → Type} [Monad m] [Lean.MonadError m] : Aesop.PhaseSpec → m Nat

Equations

• One or more equations did not get rendered due to their size.
• x.getSimpPrio = Lean.throwError (Lean.toMessageData "aesop: simp builder can only construct 'norm' rules")

def Aesop.RuleBuilder.simpCore (decl : Lean.Name) (phase : Aesop.PhaseSpec) : Lean.MetaM Aesop.LocalRuleSetMember

Equations

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

def Aesop.RuleBuilder.simp : Aesop.RuleBuilder

Equations

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