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

## Instances For

## Equations

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

## Instances For

## Equations

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