bug in hover tooltips?

Stream: general

[Johan Commelin]

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?