Zulip Chat Archive

Stream: new members

Topic: notation


view this post on Zulip Michael Beeson (Sep 21 2020 at 21:07):

Section 6.6 of Theorem Proving in Lean says,

Lean’s core library declares the left-binding powers of a number of common symbols.
https://github.com/leanprover/lean/blob/master/library/init/core.lean
You are welcome to overload these symbols for your own use, but you cannot change their binding power.

That seems to be false--in my ignorance I declared binding powers for some of these operators
at the top of my first file. If I remove those lines there's no problem with the parsing, indicating that
infix is still ok, but my proofs no longer check, indicating that the binding powers I had declared
were in force, rather than the defaults, before I removed those lines. Put those lines back, of
course the project builds again.

view this post on Zulip Pedro Minicz (Sep 22 2020 at 00:59):

I also believe that to be false. You _can_ change the binding power. Maybe what the book means is that you _probably_ shouldn't.

view this post on Zulip Pedro Minicz (Sep 22 2020 at 01:00):

For reference, this is an thread where redefining the binding power of existing notation fixed a problem I was having: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Substitution.20notation

view this post on Zulip Pedro Minicz (Sep 22 2020 at 01:00):

Also. It is always possible that it wasn't possible when the book was written.

view this post on Zulip Jeremy Avigad (Sep 22 2020 at 15:57):

The statement was probably true when it was first written. Lean changed a lot over the years, and I am guessing that this changed and nobody noticed (until now) that the documentation was out of date. I'll fix it.


Last updated: May 14 2021 at 07:19 UTC