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: Dec 20 2023 at 11:08 UTC