advantage of `notation` over `def`?

Stream: new members

[Adam Dingle]

In Lean, I can write either

notation "ℕ" => Nat

or

def ℕ := Nat

They seem to have approximately the same effect. After either declaration, I can write

variable (a b c : ℕ)

#check a
#check ℕ

and the results are the same in either case.

Is there some practical reason to favor notation over def when introducing a synonym such as this?

[Kevin Buzzard]

Try #synth Add \N in both cases to see a difference. Parts of lean's inner workings work up to syntactic equality and other parts up to definitional equality. With notation \N and Nat are syntactically equal,. With def they're only definitionally equal. The typeclass inference system (used by #synth) works up to syntactic equality, as does the rw tactic.

[Kevin Buzzard]

See the relevant part of my course notes for more information about the three kinds of equality in play in lean

[Adam Dingle]

This is very helpful - thanks!

[Junyan Xu]

notation can also "carry variables around" (so it works as a replacement of Lean 3's parameter): if you have an expression that depends on some variables, if you make a def for that expression, you have to make those variables arguments, either explicit (so you need to supply them every time you use the def), or implicit (which Lean may fail to infer). But if you make the whole expression a notation, then it just works (like hard-coded (rather than inferred) implicit arguments).

[Jireh Loreaux]

@Adam Dingle see also this