Delaborator priority

Stream: lean4

[Jon Eugster]

Is there a way to specify delaborator priority?

Say I wanted to overwrite an existing delaborator in my project, I would try to do something like this:

@[delab app.Finset.sum]
-- or `@[app_delab Finset.sum]` but I think that's irrelevant
def delabFinsetSum' : Delab :=
  whenPPOption getPPNotation <| withOverApp 5 <| do
    _ -- modified delaborator

But it seems the original delaborator takes priority by default.