Zulip Chat Archive

Stream: general

Topic: bug in hover tooltips?


view this post on Zulip 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: May 06 2021 at 21:09 UTC