notation observation

Stream: general

[Kevin Buzzard]

When I was a beginner I used #print notation a lot, to get my head around the absolute basics (e.g. "what the heck is ≃" or "I wonder what the actual definition of = is?"). But there are just a few pieces of notation for which this doesn't work and you have to learn them manually. → and ∀ give unhelpful outputs (no notation) and I remember being frustrated by ⋃ and other big operators:

import tactic

#print notation ⋃ -- `⋃`:1024 binders `,`:0 (scoped 0) := #0

because that answer is not at all helpful (the correct answer is set.Union). However I just noticed that depending on order of imports you can make the output even less helpful:

import data.set.lattice
import set_theory.zfc -- switch order of inputs to get back to original unhelpful answer

#print notation ⋃
/-
`⋃`:1024 :=
  | Set.Union
  | Class.Union
-/

(note that Set.Union is not set.Union).

Can we do any better in Lean 4 for beginners?

[Sebastian Ullrich]

Lean 4 does not have #print notation, but your last example shows that it is better to interact with actual usages of the notation to learn about it. For which Lean 4 provides go-to-definition & docstring hover. image.png

[Kevin Buzzard]

I see -- so for example if I see notation on github which I don't understand I should just find the relevant file in a local copy of a repo.

[Sebastian Ullrich]

I'd say so, yeah. You need at least the right imports anyway, after all.

[Sebastian Ullrich]

Ideally of course you'd jump right there from GitHub using Gitpod/GH Codespaces

[Yaël Dillies]

If Lean 4 doesn't have #print notation, how do you figure out the precedence of an operator?

[Kevin Buzzard]

you can see it in the screenshot

[Yaël Dillies]

Sure, but how do I check a bunch of precedences at once/how do I know which notations are used?

[Yaël Dillies]

And how do I know which operators have a given precedence? We will crucially need this soon to fix the precedences of order vs algebraic operators as we talked about a few times already.

[Mario Carneiro]

A tool to dump all syntax, or all syntax in a given syntax category like term, sounds doable in lean 4 (this is lean 3 #print notation with no arguments IIRC)

[Gabriel Ebner]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/analogue.20of.20.23print.20notation and https://gist.github.com/pcpthm/b88152daeeb684948d768766a49f2534