## 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.

#### Reid Barton (May 21 2020 at 18:56):

Is that really the only problem with |, though? It also triggers the equation compiler

#### Johan Commelin (May 21 2020 at 18:57):

We could use \| for that :oops:

#### Patrick Massot (May 21 2020 at 18:57):

I don't think I ever had Lean thinking I wanted the equation compiler

#### Gabriel Ebner (May 21 2020 at 18:57):

What is |)?

#### Patrick Massot (May 21 2020 at 18:57):

Lean must have noticed I never use the equation compiler

#### Patrick Massot (May 21 2020 at 18:58):

See? Gabriel doesn't even know that thing

#### Reid Barton (May 21 2020 at 18:58):

I had to look them up.

#### Gabriel Ebner (May 21 2020 at 18:58):

Oh, wow. |) is ascii for ⟩ in case anybody's wondering.

#### Patrick Massot (May 21 2020 at 18:58):

Exactly. Let's get rid of ASCII art

#### Gabriel Ebner (May 21 2020 at 18:59):

If we remove |), can we then make | syntax for dvd?

#### Mario Carneiro (May 21 2020 at 19:01):

aren't there issues with the other meanings of | too though?

#### Mario Carneiro (May 21 2020 at 19:01):

like in set builders, the equation compiler, and inductive cases

#### Patrick Massot (May 21 2020 at 19:02):

I'm using | for absolute value throughout the tutorials project, and the only issue is with (| and |)

#### Gabriel Ebner (May 21 2020 at 19:03):

Ok, I'll let you figure out how to use it in mathlib.

#### Patrick Massot (May 21 2020 at 19:03):

Note that I'm not advocating setting a global abs notation

#### Gabriel Ebner (May 21 2020 at 19:05):

Well, it's gone in 3.15: lean#265

#### Patrick Massot (May 21 2020 at 19:07):

When I see PR pages like lean#265 I wonder whether Gabriel is also bors.

#### Kevin Buzzard (May 21 2020 at 23:40):

You never see them in the same place at the same time

Last updated: May 08 2021 at 03:17 UTC