Email Gateway (Aug 19 2022 at 12:42): 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".
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: Nov 21 2024 at 12:39 UTC