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



Am 26.11.2013 13:06, schrieb Peter Lammich:
Hi,

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

theory Scratch
imports Complex_Main
begin

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


when hovering over the a in "a+b" and pressing Ctrl, I get the following
tooltip:
   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
begin

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"

end

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.

Dmitriy




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