Delaborator weird behavior

Stream: lean4

[jthulhu]

I've tried to convert existing unexpanders in my code to conditional unexpanders, ie. unexpanders that can be turned on/off with an option.

I have the following code

def lift (α : liftedU) : Type _ := ...

register_option pp.lift : Bool := {
  defValue := false
  group := "pp"
  descr := "(pretty printing) display lift from object-level types to Lean types"
}

@[delab app.lift]
def delab_lift : Delab := do
  whenNotPPOption (·.get pp.lift.name pp.lift.defValue) do
    let e ← getExpr
    guard <| e.isAppOfArity' ``lift 1
    let arg ← withAppArg delab
    `($arg)

This doesn't work though, in the sense that, even if pp.lift is false, the delaboration never happens. If, instead, I fully specify the name of lift, as such @[delab app.Tltt.Hott.lift], it works. This looks like a bug, but I'm not sure.
@Kyle Miller

[Kyle Miller]

The delab attribute expects what comes after app to be the fully qualified name for the constant

[Kyle Miller]

One way you can tell whether it's correct is to hover your mouse over the app...., since for convenience if the constant exists then the delab attribute makes it hoverable.

[Kyle Miller]

Feel free to create a Lean issue with a feature request that @[delab app.lift] should resolve the name lift to Tltt.Hott.lift and then instead add a delaborator with the key app.Tltt.Hott.lift.

[Kyle Miller]

(You can take a look at docs#Lean.PrettyPrinter.Delaborator.getExprKind to see why it works the way it does.)

[jthulhu]

Here is the corresponding RFC: #4899.

[Kim Morrison]

(Completed in lean#4976.)