## 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: May 06 2021 at 21:09 UTC