Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Misleading tooltips on Isabelle-Terms with coe...


view this post on Zulip Email Gateway (Aug 19 2022 at 12:42):

From: Peter Lammich <lammich@in.tum.de>
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".

view this post on Zulip Email Gateway (Aug 19 2022 at 12:42):

From: Dmitriy Traytel <traytel@in.tum.de>
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


Last updated: Mar 28 2024 at 16:17 UTC