Zulip Chat Archive

Stream: new members

Topic: Looking up definitions of symbols

Aniruddh Agarwal (May 21 2020 at 15:31):

Is there a good way of looking up the definitions of ∈, |, ∃, etc.?

Bryan Gin-ge Chen (May 21 2020 at 15:44):

#print ∈ will show the declaration name. I think you can also right click on them and go to definition as usual.

Bryan Gin-ge Chen (May 21 2020 at 15:48):

These are all defined as notation typeclasses though so the definitions won't be too helpful. unfortunately I don't know of a quick way to find the actual instance that's at play when they're being used in a block of code other than digging through set_option trace.class_instances true output.

Jalex Stark (May 21 2020 at 18:30):

huh for some reason I've been writing print notation ∈ instead, it seems they have the same output

Aniruddh Agarwal (May 21 2020 at 18:40):

Emacs seems to be inconsistent with which symbol's definitions it can automatically look up and display and which it can't. I should read lean-mode's documentation more closely to see if I'm missing something

Bryan Gin-ge Chen (May 21 2020 at 18:42):

The Lean server frequently has trouble with go-to-definition when working in tactic mode. I don't know if there's a good solution for this.

Aniruddh Agarwal (May 21 2020 at 18:43):

I was very confused about why lean didn't like #print |. Turns out I should've been typing #print \|. /sigh

Johan Commelin (May 21 2020 at 18:46):

Yup, that one is annoying.

Reid Barton (May 21 2020 at 18:49):

You can use C-u C-x = to find out what character you have, and how to type it.

Patrick Massot (May 21 2020 at 18:52):

Oh, it makes me think of a great improvement we could make in Lean 3.15.0. Could we get rid of (| and |)? This would allow declaring | (the regular ASCII one) as notation for the absolute value without fearing to put it next to a parenthesis.