[isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit
when giving the semantics tutorial this morning, I ran into quite
strange tooltips in Isabelle/jedit: Consider,
term "∃a::nat. ∃b::real. a+b=0"
when hovering over the a in "a+b" and pressing Ctrl, I get the following
This tooltip is simply wrong! The variable a still has type nat. So I
would have expected either a::nat, or "real a :: real".
This archive was generated by a fusion of
Pipermail (Mailman edition) and