Automatically desugar unicode notation

Stream: lean4

[Phillip Harris]

Hi all,

I was reading this old thread

https://leanprover-community.github.io/archive/stream/270676-lean4/topic/analogue.20of.20.23print.20notation.html

which contains a utility that lets you automatically desugar the definition of a unicode symbol:

https://gist.github.com/pcpthm/b88152daeeb684948d768766a49f2534#file-print_notation-lean-L8

however, it seems to be written in an old version of Lean and doesn't work anymore.

Is there any update on this problem? If I want a way to desugar some notation automatically is fixing the above code my best bet? (Also, the reason I want to do this is I'm trying to automatically remove open declarations and qualify every name, and I can't qualify unicode symbols by putting "MyNamespace." in front of them. )

Thanks,
Phillip

[Damiano Testa]

Could you give an example? Does mathlib's #find_syntax "mySymbol" help?

[Phillip Harris]

For example the symbol 𝓝, it seems to be in the Filter namespace but you can't write `Filter.𝓝

I didn't know about #find_syntax, that seems like what I'm looking for. Though I tried it just now on 𝓝 and it took almost 10 minutes... not sure why. Edit: Actually I'm a little confused about what this command returns? It seems to return objects of type Lean.ParserDescr and not the definition of 𝓝 itself, which would be nhds

[Michael Rothgang]

Your question aside: are you sure you want to remove every open statement? Outside of minimization, that doesn't seem useful --- notation is there to improve readability.

[Michael Rothgang]

Ideally, each notation should have documentation showing that it denotes (if not, that's a "bug" in the notation).

[Phillip Harris]

It's for ML. The LLMs have trouble learning the namespaces.

[Kyle Miller]

Not sure if it's helpful, but maybe the LLMs can learn to do open scoped Filter to enable the filter notation without also opening the namespace?

[Phillip Harris]

Hmm, that might be good enough. Maybe I can just take all the commonly used notations that are defined with scoped notation and don't overlap and open all of them at the start.