importing mathlib breaks syntax

Stream: lean4

[Tomaz Mascarenhas]

Hi, the following snippet is parsed correctly:

section foo

def xss : List (List Nat) := [[2]]
#eval xss[0]![0]!

end foo

However, if I import this file from mathlib, I get an error:

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

section foo

def xss : List (List Nat) := [[2]]
#eval xss[0]![0]! --unexpected token '!['; expected command

end foo

I believe this is caused by some notation defined in the mathlib file that conflicts with the get! notation. Is there a way to import just the definitions from the mathlib file, without the notation? Or maybe another way to fix this problem so I can have both the notation and the import?

[Floris van Doorn]

I expect that this conflicts with the ![a, b, c] notation for vectors in Mathlib (in a much lower-level file).
The answer is that currently it's not possible to not import notation.

[Floris van Doorn]

Is (xss[0]!)[0]! acceptable as a workaround for now?

[Tomaz Mascarenhas]

I think so, thanks!

[Floris van Doorn]

Only marginally related, @Lean core team: Maybe xss[0, 0]! would be nice notation for this?

[Eric Wieser]

Can we change the precedence to fix this?

[Eric Wieser]

Or perhaps split the token in two

[Robin Arnez]

Yeah, right, "!" noWs "[" for example

[Jireh Loreaux]

I think the vector notation should also be scoped (regardless of any other fixes we might choose).

[Eric Wieser]

Is v[...] or #[...] notation scoped?

[Jovan Gerbscheid]

I'd rather keep ![...] global in the same way as #v[...] and #[...]

[Jovan Gerbscheid]

Somewhat unrelatedly, what happened to the nice plan of making ![...] reduce to a recursor in reducible transparency, so that its applications can be reduced in rw and type class search?

[Kenny Lau]

similarly I don't think scoping notations is the solution to every problem. maybe putting atomic on ]! or ![ might solve the problem?

[Jovan Gerbscheid]

Doesn't the tokenization happen before parsing? So changing the parser wouldn't fix the problem of getting the wrong token?

[Robin Arnez]

Yes, we need to avoid getting a "![" token in the first place, so separating them into two tokens in the ![...] parser is the way to go.

[Jireh Loreaux]

Kenny Lau said:

I don't think scoping notations is the solution to every problem.

I think we should scope virtually all notations, maybe with a feature to have some scopes open by default, but also with the ability to close scopes. (And as I said, this is orthogonal to whether we implement other fixes to this specific issue.)

[Kenny Lau]

I would also complain less if the docgen opens scoped syntax