## Stream: general

### Topic: notation observation

#### Kevin Buzzard (Mar 04 2022 at 12:27):

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 (Mar 04 2022 at 12:45):

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 (Mar 04 2022 at 12:51):

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 (Mar 04 2022 at 13:08):

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

#### Sebastian Ullrich (Mar 04 2022 at 13:11):

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

#### Yaël Dillies (Mar 04 2022 at 13:16):

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

#### Kevin Buzzard (Mar 04 2022 at 13:16):

you can see it in the screenshot

#### Yaël Dillies (Mar 04 2022 at 13:42):

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

#### Yaël Dillies (Mar 04 2022 at 13:43):

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 (Mar 04 2022 at 14:11):

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 (Mar 04 2022 at 14:42):

Last updated: Dec 20 2023 at 11:08 UTC