Zulip Chat Archive

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):

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

Last updated: Aug 03 2023 at 10:10 UTC