absolute value

Stream: lean4

[Patrick Massot]

In mathlib3 we have notation `|`a`|` := abs a which is absolutely needed, but the naive Lean4 version confuses the parser when defining inductive types mathlib4#477. What is the correct notation incantation here?

[Gabriel Ebner]

See https://github.com/leanprover-community/mathlib4/issues/307 and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathport.20abs.20syntax.20clash

[Patrick Massot]

Sorry, I forgot we already had that conversation. The answer is still the same: this is a really serious issue if we can't get that notation to work. In particular for me it makes Lean 4 a lot less suitable for teaching . @Leonardo de Moura

[Sebastian Ullrich]

What about introducing whitespace sensitivity?

macro atomic("|" noWs) a:term noWs "|" : term => `(abs $a)
#check |a|
def test : Nat → Nat
  | 0 => 0
  | n + 1 => 0

[Patrick Massot]

That's certainly better than nothing or a weird notation, at least if the error message when there is an extra whitespace is somewhat understandable (or at least constant).

[Sebastian Ullrich]

"Not great, not terrible" I'd say

#check | 1 + 1|
     --^ "expected no space before"
#check |1 + 1 |
            --^ "expected no space before"

[Sebastian Ullrich]

The error position in the first case is an unfortunate consequence of the necessary atomic

[Patrick Massot]

It's totally fine!

[Patrick Massot]

I just tested it and was very pleased

[Kevin Buzzard]

In Lean 3 we use \| for division; could we not move to this for abs?

I will remind you Patrick that Mario has always said that bracket-like notation which doesn't have distinct symbols for the left and right side are a parsing disaster. However I'm well aware that this notation is standard and non-negotiable in mathematics :-/