analogue of #print notation

Stream: lean4

[Kevin Buzzard]

What is the Lean 4 analogue of #print notation?

I ask because I was just completely confused when porting some logic.basic stuff from Lean 3 to Lean 4 and I was all over the shop trying to deal with a heq lemma and ultimately it was because == turns out not to mean HEq in Lean 4 but BEq, boolean equality.

PS I see now that I could at least have discovered that == wasn't HEq by using the pretty printer to discover that HEq is ≅, a design decision which the mathematicians might be quite interested in...

[Brandon Brown]

Yeah I would like to know as well. I was sleuthing through the Lean4 code base and couldn't find anything

[Mario Carneiro]

I would be in favor of using no notation for HEq

[Mario Carneiro]

that should make it clear which one is preferred

[Mario Carneiro]

(of course people can reintroduce their own notation if they like, in which case ≅ as a local or scoped notation will not be nearly as contentious)

[Gabriel Ebner]

That looks more like isomorphism than equality to me.

[Kevin Buzzard]

In mathematics it is used as a relation on types not terms, so it looks funny to me, but on the other hand we've already seen that notation in computer science and mathematics clashes sometimes (eg => )

[Mario Carneiro]

there is always ===...

[Sebastian Ullrich]

Regarding the original question, we should soon have go-to-definition and on-hover documentation for arbitrary syntax, including notations (someone still has to write all those doc comments afterwards of course...). I assume that would more than make up for the lack of the command?

[Sebastian Ullrich]

The Lean 3 syntax also doesn't make as much sense in Lean 4 since it is much less focused on tokens to begin with (see e.g. per-parser precedence).

[Kevin Buzzard]

Yes, go-to-definition would certainly solve my initial problem! I have also really got to internalise this "if you can't figure it out, get grepping through the source code" approach, which is not something I instinctively do because I was spoilt by Lean 3's more mature state when I started learning it. Thanks.

[pcpthm]

I worte a custom command <https://gist.github.com/pcpthm/b88152daeeb684948d768766a49f2534> but I think go-to-definition is a better solution.

[Kevin Buzzard]

Thanks! So now I can do `#print_notation "a == b" and it tells me where to look in the lean 4 repo to see the definition of the notation (as opposed to grepping for the symbol where of course you also end up with all the uses of it).