Suppressing generalized dot notation.

Stream: mathlib4

[Wrenna Robson]

Hey. I have a family of equivalence on Nat parameterised by a Nat - so I'm in the Nat namespace. But I don't really want my equivalence to use that parameter for the dot notation - like, if I have def MyEquiv (i : Nat) : Nat \equiv myType, I don't want Lean/the VS code display to default to displaying (I.MyEquiv) - it is inconsistent with other ways I use dot notation in the same file. Is there a way to get it to, well, not?

[Yaël Dillies]

I believe pp_no_dot has not been restored after pp_dot became the default again. So, unless I'm wrong, no you can't

[Wrenna Robson]

RIP.

[Wrenna Robson]

Alas.

[Wrenna Robson]

I just tried set_option pp.fieldNotation.generalized false, but it seems it is forbidden by a linter.

[Yaël Dillies]

You can also disable the linter :upside_down:

[Wrenna Robson]

lol

[Markus Himmel]

Yaël Dillies said:

I believe pp_no_dot has not been restored after pp_dot became the default again. So, unless I'm wrong, no you can't

I don't think this is true, @[pp_nodot] should work.

[Martin Dvořák]

Speaking of suppressing the dot notation, I wish I could disable A.fromBlocks B C D and other declarations that have several arguments of the type in the prefix.

[Wrenna Robson]

Markus Himmel said:

Yaël Dillies said:

I believe pp_no_dot has not been restored after pp_dot became the default again. So, unless I'm wrong, no you can't

I don't think this is true, @[pp_nodot] should work.

How do you use this with simps?

[Wrenna Robson]

like if I already have @[simps!] at the start

[Wrenna Robson]

ah, comma

[Jon Eugster]

Indeed, @[pp_nodot] does work, but I quickly checked and there is some syntax in Mathlib.Mathport.Syntax that prevents it from working:

-- import Mathlib.Mathport.Syntax -- uncomment me to fail

@[pp_nodot] def Nat.sin (x : Nat) : Nat := 0

variable (n : Nat)

#check n.sin

I'll make a quick PR!

[Wrenna Robson]

It seems to work in that the display of it changes, but yes it doesn't fully lock it off.

[Jon Eugster]

#14090

[Markus Himmel]

This is already addressed in #13781, which is on the queue.

[Jon Eugster]

Ah, I looked at that PR and thought it was already done merging without that fix :sweat_smile:

[Kyle Miller]

Yaël Dillies said:

I believe pp_no_dot has not been restored after pp_dot became the default again.

While the release notes don't include everything, pp_nodot is mentioned: https://github.com/leanprover/lean4/blob/master/RELEASES.md

It's also in the blog post for the release: https://lean-lang.org/blog/2024-6-1-lean-480/

[Yaël Dillies]

Ah, glad to see I am wrong!

[Kyle Miller]

(It's hard to find, but there's a bit of documentation in the description for the pp.fieldNotation option too.)

[Yaël Dillies]

Ah, I see where I got confused: pp_nodot was reintroduced but the corresponding lines in Mathlib were not uncommented

[Kyle Miller]

No one seemed to want to merge my PR for the last few weeks :-(

In any case, there are a number of places to figure out for certain whether pp_nodot exists so there's no need to try to go by memory :-)

[Yaël Dillies]

What PR? I will review it (assuming it's to mathlib4)

[Ruben Van de Velde]

Didn't it just land? #13781