Mathport abs syntax clash

Stream: mathlib4

[Alexander Bentkamp]

The notation for abs clashes with some variants of the match notation:

import Mathbin.Algebra.Abs -- works if this is not imported

def test : Nat → Nat
| 0 => 0  -- expected '|'
| n + 1 => 0

Is there a way to switch off a notation that has already been introduced? Should I report this as a bug on the mathport GitHub?

[Gabriel Ebner]

Yes, we can change the notation during the port.

[Alexander Bentkamp]

ok, I'll open an issue on GitHub.

[Alexander Bentkamp]

https://github.com/leanprover-community/mathport/issues/73

[Eric Rodriguez]

the abs notation is even weird in Lean3, where often you need to do (|x|) instead of just |x|. I wonder if there's another vertical bar we could use for abs?

[Henrik Böving]

There is ∣ typed as \mid in the emacs Lean input method.

[Mario Carneiro]

that one is already in use for divides

[Mario Carneiro]

I will once again renew my suggestion to stop using symmetric bracket pairs and use ⸡x⸠ like in mathematica

[Eric Rodriguez]

why is it so important that they're asymmetric? is it because of how Lean's parser works? I don't currently like that syntax but I could get used to it I think

[Mario Carneiro]

Symmetric brackets are fundamentally ambiguous

[Mario Carneiro]

last time this came up I used an example like |1+|1-1|+|-|1|||

[Patrick Massot]

In practice this simply doesn't arise

[Patrick Massot]

So there is nothing to worry about.

[Patrick Massot]

We have hundreds of year of training in putting parentheses when needed.

[Mario Carneiro]

In practice this particular notation has been singled out as causing problems on several occasions

[Eric Rodriguez]

I see, a human would then work backwards from the totasl number of |s in a line if something as horrid as this came up but that doesn't seem good for a computer parser at all

[Mario Carneiro]

The issues that arise in practice are slightly different in expression, but fundamentally the issue is that you can't make a totally coherent parser for symmetric brackets because they are ambiguous

[Patrick Massot]

I haven't seen realistic examples where this is an issue, but I may have missed them.

[Mario Carneiro]

the issue that arises in lean 3 is that you can't give the brackets the right precedence so you need to use parens

[Mario Carneiro]

in lean 4 it looks to be much worse because you are also colliding with some built in notation

[Mario Carneiro]

I believe this was also why we had to remove the ascii structure brackets (|a, b, c|)