Dot notation failing me

Stream: general

[Yaël Dillies]

Today, I've been let down by dot notation. And it hurts.

import data.equiv.basic

#check equiv.set.compl -- works
#check equiv.refl _ -- α ≃ α
#check (equiv.refl _).set.compl
/-
invalid field notation, 'set' is not a valid "field" because environment does not contain 'equiv.set'
  equiv.refl ?m_1
which has type
  ?m_1 ≃ ?m_1
-/

Any way we can get back along?

[Eric Wieser]

There are two ways out of this; rename set.compl to set_compl, or use the hack I suggested in the ideal.quotient.mk thread

[Kyle Miller]

equiv.set.compl works because it's doing plain old namespace lookup, and (equiv.refl _).set.compl doesn't work because the extended dot notation starts with (equiv.refl _).set so tries to look for a thing called equiv.set. Namespaces aren't "things".

I think there are some runtime complexity reasons not to have it then followup with trying to look for equiv.set.compl, though I'm not sure why namespaces can't be "things" for the purpose of dot notation.

I'm wondering if the following would be a sensible extension to Lean (if a bit hacky) so that it's possible to say how you want the dot notation to be interpreted:

#check (equiv.refl _).«set.compl»

The hack is that guillemets are already used for symbol quotations, but the . is being intentionally reinterpreted as a dot:

#check equiv.set.«compl» -- works
#check equiv.«set.compl» -- doesn't work

[Mario Carneiro]

I wouldn't suggest using the guillemets like that; the whole point is so that you can have . as a legitimate character in a name component, so parsing them for dots would defeat the purpose - it would make it impossible to have an actual name component with a dot in it (there are no "second level guillemets")

[Kyle Miller]

@Mario Carneiro I agree it's a questionable idea, but this would only apply to the extended dot notation, so it might be OK. An alternative is using another symbol for extended dot notation, like (equiv.refl _)!set.compl, but so many symbols already have a use.

If you really wanted the quoted dot, then you'd still be free to write equiv.«set.compl» (equiv.refl _) for example.

[Mario Carneiro]

Did you know that ^. also does dot notation - it was the original syntax before we moved to . which has ambiguity with namespaces

[Kyle Miller]

Oh, nice, so it's already been solved :smile:

#check (equiv.refl _)^.set.compl

[Yaël Dillies]

Ohohoh! A new trick for me :stuck_out_tongue_wink: