Re: [isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit

Am 26.11.2013 13:06, schrieb Peter Lammich:

when giving the semantics tutorial this morning, I ran into quite
strange tooltips in Isabelle/jedit: Consider,

theory Scratch
imports Complex_Main

term "∃a::nat. ∃b::real. a+b=0"

when hovering over the a in "a+b" and pressing Ctrl, I get the following
   bound "a"
   bound variable
   :: real

This tooltip is simply wrong! The variable a still has type nat. So I
would have expected either a::nat, or "real a :: real".
The tooltip is right! The variable a has type real in the above example. It is the usual confusion with the map function on functions (which is contravariant in the first argument). The following shows more precisely what happens there.

theory Scratch
imports Main

declare [[coercion_enabled]]
declare [[coercion int]]
declare [[coercion_map "λf g h. g o h o f"]]

term "∃a::nat. ∃b::int. a+b=0"


As opposed to this example the map function as defined in Real.thy has the composition unfolded---this simplifies proofs but has confused many users in the past (showing the beta reduced term). We should reconsider whethere this map function should be enabled by default at all.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.