Zulip Chat Archive

Stream: general

Topic: bug in hover tooltips?


Johan Commelin (Mar 15 2021 at 04:09):

import logic.basic

variables (cond : )

example : cond = 0 :=
sorry

If you hover over cond in the example you get the type of _root_.cond about booleans. Is this to be expected? Is this a known thing?


Last updated: Dec 20 2023 at 11:08 UTC