Natural abs syntax clashes with pattern matching

[abentkamp]

trafficstars

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

[gebner]

Discussion on zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathport.20abs.20syntax.20clash

[gebner]

Transferred to mathlib4 because we've solved the issue in mathport (by just ignoring the notation).

We still need to figure out a notation for the absolute value in Lean 4 though.

[gebner]

#477 added the |abs| notation.