| open Lean PrettyPrinter | |
| namespace ns | |
| inductive Foo | mk: Foo | |
| @[app_unexpander Foo.mk] | |
| def unexpadFoo : Lean.PrettyPrinter.Unexpander | `($x) => `(unexpand) | |
| def foo := Foo.mk | |
| #print foo | |
| @[app_unexpander ns.Foo.mk] | |
| def unexpadFoo' : Lean.PrettyPrinter.Unexpander | `($x) => `(unexpand) | |
| def bar := ns.Foo.mk | |
| #print bar | |
| end ns |