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