Is there a way to quickly check the definition?

Stream: new members

[jsodd]

Is there a quick way of checking how, say, an inner product is defined? Here's an example: I want to see what these two definitions expand to without going to the documentation:

import Mathlib
variable {x y : EuclideanSpace ℂ n}
#check ⟪x, y⟫_ℝ
#check ⟪x, y⟫_ℂ

[Yaël Dillies]

If you guess how they are defined, you can do

lemma foo : ⟪x, y⟫_ℝ = ∑ _ ∈ _, _ := rfl
#check foo

[jsodd]

Well, if I could always guess the definitions, I probably wouldn't need this :smile:

[Yaël Dillies]

My point is that you only need to know what the outermost symbol is (eg the above works for both ⟪x, y⟫_ℂ := ∑ i, conj (x i) * y i and ⟪x, y⟫_ℂ := ∑ i, x i * conj (y i) . In this specific case, since there is no notation typeclass you can just Go to definition by eg Ctrl+click

[jsodd]

Well, even the outermost symbol depends on the way things are implemented in mathlib, which I don't expect to be in perfect correspondence to how I think about them. And trying out several choices quickly gets slower than looking for the definition in the docs.

[jsodd]

By the way, your code doesn't work for me, maybe I forgot to open something...

[Yaël Dillies]

I mean, I would usually just look in the docs, but you asked for a doc-less way :shrug:

[jsodd]

I honestly thought there would be something like #eval# or #print for this...

[Sebastian Ullrich]

What's wrong with the mentioned Go to definition?

[jsodd]

If you click on Go to definition (on the brackets or on what?), lean first sends you to the definition of inner product notation, then to the general inner products and so on. There seems to be no easy way to see the exact way it is defined in the current context

[jsodd]

You can go to the definition of EuclideanSpace instead and then go through the definitions of PiLp and WithLp just to find how the inner product is defined

[jsodd]

Seems to be too much for a thing that simple

[Daniel Weber]

#reduce ⟪x, y⟫_ℝ
shows the definition, but at a very low level

[Daniel Weber]

#whnf ⟪x, y⟫_ℝ, perhaps?

[Sebastian Ullrich]

A new command would have to make the exact same decisions of what to unfold and what not, there is no straightforward answer here. The one tool other than unfolding nothing we have is to unfold everything, which is #reduce as just mentioned

[jsodd]

Let's say I've redefined it for myself somewhere, but don't remember where. I'd like to be able to quickly check

[Daniel Weber]

import Mathlib
variable {n : Type*} [Fintype n] {x y : EuclideanSpace ℂ n}
#simp => ⟪x, y⟫_ℝ

works in here, but that's only thanks to the simp lemma docs#PiLp.inner_apply

[jsodd]

Sebastian Ullrich said:

A new command would have to make the exact same decisions of what to unfold and what not, there is no straightforward answer here. The one tool other than unfolding nothing we have is to unfold everything, which is #reduce as just mentioned

Maybe some command which would allow me to manually unfold it? Just without guessing names of what must be unfolded