simproc priority

Stream: lean4

[Alex Keizer]

For a regular simp-lemma, we can give it a low priotity by writing @[simp(low)]. Is there an analogue of this for (d)simprocs?

I tried writing dsimproc [simp(low)] reduceIsRefinedBy (_ ⊑ _) := ..., but that doesn't seem to be valid syntax. I also tried putting (priority := low) at various spots, but none of those were valid either.

[Eric Wieser]

Isn't the normal syntax @[simp low]?

[Alex Keizer]

Both @[simp(low)] and @[simp low] seem to be legal. Sadly, dsimproc [simp low] is also not valid

[Jovan Gerbscheid]

Looking at docs#Lean.Meta.Simp.SimprocEntry, there doesn't seem to be a way to set the priority.