mathport bug with `^`

Stream: mathlib4

[Jireh Loreaux]

@Mario Carneiro I know mathport is broken right now anyway, but I think I found a bug. In the file linear_algebra.quotient, there is an occurence of P^.quotient.mk_smul in the mathlib 3 source, where P : submodule R M and this is some dot notation magic that unfolds to submodule.quotient.mk_smul P. Mathport translated this as P. I'm not sure what the ^ notation means anyway.

[Eric Wieser]

foo^.bar.baz where foo : Foo means Foo.bar.baz foo

[Eric Wieser]

As opposed to foo.bar.baz which means Bar.baz (Foo.bar foo)

[Eric Wieser]

I think this is super-ancient dot notation

[Yury G. Kudryashov]

It is present in 106 lines, 17 files.

[Yury G. Kudryashov]

at least 1 false positive.

[Mario Carneiro]

It appears to be a simple bug. This notation is already supported, but the implementation was "lightly tested"

[Mario Carneiro]

While investigating this, I noticed that ^. has a secret superpower compared to .:

def list.foo.bar {α} : list α → list α := id

#check [1]^.foo.bar -- ok
#check [1].foo.bar  -- fail, interpreted as ([1].foo).bar

[Mario Carneiro]

this superpower behavior apparently has no equivalent in lean 4: |>.foo.bar is also interpreted as |>.foo |>.bar

[Eric Wieser]

Yes, that's the power I described here:

Eric Wieser said:

foo^.bar.baz where foo : Foo means Foo.bar.baz foo