Understanding notation declarations

Stream: general

[Brendan Seamas Murphy]

Hi all! I'm kind of confused about how notation works. I have a setup like this:

constant SQL : Type
constant groupBy : SQL → SQL → SQL → SQL

notation `SELECT` `*` x := x
notation `FROM1` a := a
notation `SELECT` proj `FROM1`:1 a `GROUP` `BY` v := groupBy proj a v

And I can't write SELECT a FROM1 b GROUP BY c, I need to write SELECT (a) FROM1 b GROUP BY c. I also need the :1 after FROM1 to get it to parse at all, and I don't know why.

[Simon Hudon]

The :1 is for precedence. If the parser meets ... x + y FROM1 the precedence tells Lean whether to keep reading to the right or to build the x + y expression some more with stuff on the left