source
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")

Instances For

source
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.

Instances For

source
def Aesop.RuleBuilder.simp :
RuleBuilder
Equations

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

Instances For