def Aesop.PhaseSpec.getSimpPrio {m : Type → Type} [Monad m] [Lean.MonadError m] : 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 : PhaseSpec) : Lean.MetaM LocalRuleSetMember

Equations

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

def Aesop.RuleBuilder.simp : RuleBuilder

Equations

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