Zulip Chat Archive

Stream: lean4

Topic: appUnexpander pitfall


pcpthm (Apr 02 2021 at 18:10):

When I declare an appUnexpander involving an identifier that is not in the root namespace,
and then I change the namespace, the unexpander is not applied anymore.

namespace Test

def Special (α : Type u) := α
def special : Special Nat := (1 : Nat)

@[appUnexpander Test.Special] private def unexpander : Lean.PrettyPrinter.Unexpander
| `(Special $x) => `($x)
| _ => throw ()

-- The unexpander is applied.
-- `special : Nat`
#check special

end Test

-- The unexpander is not applied.
-- Test.special : Test.Special Nat
#check Test.special

-- Workaround: don't match against the identifier
@[appUnexpander Test.Special] private def unexpander : Lean.PrettyPrinter.Unexpander
| `($_Special $x) => `($x)
| _ => throw ()

I think this is because the quotation matching inside my unexpander definition is failing.
I could work around this issue by not matching against the identifier like the workaround above,
but I think this is confusing for users.
Could this situation be improved somehow?

Sebastian Ullrich (Apr 06 2021 at 14:48):

I'm afraid not. A purely syntactic match can only compare identifiers syntactically, or not at all. There is no magic bullet.

Mac (Apr 23 2021 at 17:53):

Sebastian Ullrich said:

I'm afraid not. A purely syntactic match can only compare identifiers syntactically, or not at all. There is no magic bullet.

Why not fully qualify names before running unexpanders? That way unexpanders could always target the fully qualified names to work. To make name output still pretty, you could then unqualify the names (as possible) after running the unexpanders.


Last updated: Dec 20 2023 at 11:08 UTC