Zulip Chat Archive

Stream: lean4

Topic: widget bug?

Johan Commelin (Sep 16 2022 at 20:19):

Consider

example {α : Type} (h : ∃i : α, i = i) : True :=
by
  trivial

and put your cursor between by and trivial. If you hover over the corresponding i in the source window, you get i : α in the popup

Now hover over the i that follows ∃, in the info view. I would expect the type i : α to show up. But instead the type of the lambda that is part of the ∃ is shown. Is that a feature or a bug?

Leonardo de Moura (Sep 16 2022 at 22:12):

I can reproduce this issue.

Johan Commelin (Sep 17 2022 at 02:47):

Shall I create a GH issue for it?

Johan Commelin (Sep 17 2022 at 03:35):

Done: lean4#1618

Last updated: May 02 2025 at 03:31 UTC