Re: [isabelle] Misleading tooltips on Isabelle-Terms with coercions in isabelle/jedit
Am 26.11.2013 13:06, schrieb Peter Lammich:
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.
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".
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