Re: [isabelle] Case-combinator allows qualified names for bound variables



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

On 31.10.2014 16:14, Peter Lammich wrote:
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.

--
   Peter



On Fr, 2014-10-31 at 15:50 +0100, Peter Lammich wrote:
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!?


--
   Peter









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