mathlib tutorial invalid notation: notation already declare

Stream: general

[Siyuan Yan]

Hi I am a learner of lean and I'm on the first exercise of mathlib tutorial. Line 260 shows an error about already declared notation. What does that mean?

-- line 260
local notation `|`x`|` := abs x

error message:

▶ 260:1-260:2: error:
invalid notation: notation already declared. Consider using 'notation (name := ...)'

the source code on github

[Alex J. Best]

Oops it looks like we need to fix the tutorials project, for now does changing it to

-- line 260
local notation (name := blah) `|`x`|` := abs x

fix it?

[Siyuan Yan]

Alex J. Best said:

Oops it looks like we need to fix the tutorials project, for now does changing it to

-- line 260
local notation (name := blah) `|`x`|` := abs x

fix it?

Fixed! thanks!

[Siyuan Yan]

@Alex J. Best why is there a blah placeholder?

[Alex J. Best]

Its because the notation already exists in another file that is imported, so we just need some name to distinguish them in the latest version of lean. For the purpose of this tutorial blah is a great name, you should be able to forget about it after this though, its not too important

[Alex J. Best]

https://github.com/leanprover-community/tutorials/pull/49 should fix this, I'm not sure who is in charge of merging to tutorials (perhaps @Patrick Massot ?)

[Johan Commelin]

@Alex J. Best Did you test if we need those lines at all? Isn't the existing notation defeq to abs?

[Patrick Massot]

It shouldn't be needed

[Alex J. Best]

Yeah I didn't test that

[Patrick Massot]

@Siyuan Yan we got distracted here and forgot to mention the key thing: if you see this error message then it means something is horribly broken in the way you use Lean. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/cannot.20build.20tutorials for explanations given to someone who hit the same issue.

[Siyuan Yan]

thanks!