Disable scoped notations during pretty printing

Stream: metaprogramming / tactics

[Thomas Zhu]

Is there any way to enable global notations but disable scoped/local notations while pretty-printing something?

#xy: I am working on a premise selector, which uses a language model to find candidate lemmas given a goal state. This means that the way goal states are printed should align with the way lemmas are printed (I can't have a goal state stating something about 𝓝 0 while all lemmas are about nhds 0). I can either have:

• Both lemmas and goal states printed with pp.notation false i.e. no notations at all. This is what I am currently doing, but creates rather awkward expressions like Eq (HAdd.hAdd a b) (HAdd.hAdd b a) instead of a + b = b + a, making the premise selector unusable beyond inside a tactic.
• Both lemmas and goal states printed with global notations but not scoped notations. I can do this on the lemma printing side, but I need the Meta.ppGoal inside a tactic to also print with global notations but not scoped notations for consistency. This is what I am asking for.
• Both lemmas and goal states printed with all notations. For this I think I need to wait for RFC lean#6050 to land (or hack a version of it), and then use scoped notations everywhere.