Better way to preserve unexpander across namespaces?

Stream: lean4

[Logan Murphy]

I'm trying to learn how to use unexpanders for pretty printing custom syntax.

When I try to introduce a simple unexpander, I find it doesn't carry over across namespaces, as per the following MWE:

import Lean

inductive Foo | bar

namespace Foo

def myFun : Foo → Nat := λ _ => 0


syntax "∣" ident "∣" : term

end Foo

macro_rules
| `(∣$t:ident∣) => `(Foo.myFun $t)

open Lean PrettyPrinter  Delaborator SubExpr

@[app_unexpander Foo.myFun]
def unexpand_myFun : Unexpander
| `(myFun $f:ident) =>  `(∣ $f ∣) -- needed for example 1
| `(Foo.myFun $f:ident) =>  `(∣ $f ∣) -- needed for example 2
| _ => throw ()

namespace Foo
-- example 1, inside namesapce Foo
example {f : Foo} : ∣f∣ = 0 := _
end Foo

-- example 2, outside namespace Foo
example {f : Foo} : ∣f∣ = 0 := _

As far as I can tell, if I want the pretty-printing to work both inside and out of namespace Foo, I need both alternatives in the implementation of unexpand_myfun , and I get the same effect if I declare the unexpander within Foo. Is there a simpler way to get it to work in both spaces? Or am I doing something wrong?

[Gabriel Ebner]

I guess that's the reason why many built-in unexpanders match on underscores, i.e., `($_ $f:ident)

[Logan Murphy]

Oooh, I see. I was getting a warning from the linter about this, but I thought it was referring to the ident rather than the function name. Works great now. Thanks Gabriel!