infoview inspects term for only one frame

Stream: lean4

[Eric Wieser]

I can't work out how to inspect the r • f in the following:

import Mathlib.GroupTheory.GroupAction.Basic

variable {α R : Type*} [Mul R] (f : α → R) (r : R) (a : α)

#check (r • f) a

if I click on the •, I get a very brief flash of information that I can't read, then I see r : R. How do I see the hover for r • f?

[Kevin Buzzard]

wooah that's weird. I tried this

import Mathlib.GroupTheory.GroupAction.Basic

variable {R : Type*} [Add R] (x y : R)

#check (x + y)

and you can just hover over the + in the infoview output for #check and see it fine. But my initial suspicion that "it's a \smul problem" is not correct: the problem also happens with this:

import Mathlib.GroupTheory.GroupAction.Basic

variable {α R : Type*} [Add R] (f : α → R) (g : α → R) (a : α)

#check (f + g) a

so + is misbehaving there. So it's a function evaluation problem?

[Eric Wieser]

Maybe this is a misfire in the thing that prevents you inspecting f a in (f a) b when f is a regular function?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

The 'only one frame' guess might be wrong: tooltips always initially show a 'Loading..' text before the Lean server replies with data; could it just be that you're seeing? In that case the issue would be that the annotation on r • f is incorrect, not that it's only shown for an instant.

[Eric Wieser]

That's very plausible