Understanding notation, infixl, infixr, prefix

Stream: lean4

[Sabbir Rahman]

I know that using infixl, infixr, prefix we can define custom operators. but I clicked on ¬ and found that not operator was defined via notation:max "¬" p:40 => Not p. Searching around, here's what I have learnt: Notation is a more featureful way to define operators. But I have two questions now

1. Is the notation syntax completely equivalent to infixl, infixr, prefix (when done in their format)? by equivalent I mean are they semantically or syntactically equivalent?
2. why was "Not" defined via notation and not prefix?

[Asei Inoue]

infix, infixr, prefix is macro of notation command

[Kyle Miller]

You should be able to "go to definition" on the infix/prefix commands to see how they're defined in terms of notation.

The resaon Not is not using a prefix is that prefix:40 "¬" => Not would be equivalent to notation:40 "¬" p:40 => Not p. The max in the notation version makes the notation not need parentheses around it even if it's placed in some high-precedence contexts. (Maybe someone can come up with some examples why it is the way it is.)

[Sabbir Rahman]

unfortunately when I tried clicking on infix/prefix vscode was not going anywhere, also tried "go to definition" that also failed.

[Kyle Miller]

Make sure you have import Lean (or a stronger import)

[Sabbir Rahman]

Ah thanks, I was actually browsing the .elan/toolchains/leanprover--lean4---v4.16.0/src/lean/Init/Notation.lean file and was clicking on infix there and that wasn't working. After writing infix in a scratch file with import Lean that worked