Email Gateway (Aug 19 2022 at 16:14): Email Gateway (Aug 19 2022 at 16:14):From: Peter Lammich <lammich@in.tum.de>
Referring to Isabelle-2014
Hi, I recently encountered the following (strange) behaviour:
theory Scratch
imports Main begin
term "case a of Some Foo.bar ⇒ Foo.bar"
The term is accepted, and "Foo.bar" is highlighted as a bound variable.
I would have expected that bound variables cannot have qualified names!?
Email Gateway (Aug 19 2022 at 16:14):From: Peter Lammich <lammich@in.tum.de>
There is something even more weird going on:
theory Scratch
imports Main begin
datatype bar = foo
declare [[show_types]]
notepad begin
fix foo :: nat and a
term "case a of Some (foo) ⇒ foo"
(* "case a∷nat option of Some (foo__∷nat) ⇒ foo__"
:: "nat" *)
Note that, in the above term, "foo" is a bound variable!
However, it's type is restricted to nat by the type inference (Expected:
'a).
Moreover, in the isabelle/jedit text area, the syntax highlighting is
completely wrong:
The first "foo" (in "Some foo") is highlighted as constant. The second
"foo" is highlighted as fixed variable. Also the tooltips you get by
hovering over the "foo"s show the same wrong(!) information.
Email Gateway (Aug 19 2022 at 16:40):From: Dmitriy Traytel <traytel@in.tum.de>
This behaviour is quite old (e.g. already presend in Isabelle2012). I
guess this is just a side effect of being able to disambiguate
constructors by long names.
Probably, it should be handled similarly to lower case theory names:
don't (mis)use it, since one day the ability to write it might disappear.
Dmitriy
Email Gateway (Aug 19 2022 at 16:41):From: Dmitriy Traytel <traytel@in.tum.de>
Yes, the tooltip and the highlighting is indeed wrong. This is an
unlucky interplay between, the case translation and the auto fixes. Of
course, easy to avoid by not using the same name for everything (or
referring by the long name to the constructor).
Dmitriy
Last updated: Apr 20 2024 at 08:16 UTC