Re: [isabelle] Case-combinator allows qualified names for bound variables
- To: cl-isabelle-users at lists.cam.ac.uk, Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] Case-combinator allows qualified names for bound variables
- From: Dmitriy Traytel <traytel at in.tum.de>
- Date: Mon, 03 Nov 2014 09:57:39 +0100
- In-reply-to: <1414768469.30420.12.camel@lapbroy33>
- References: <1414767041.30420.5.camel@lapbroy33> <1414768469.30420.12.camel@lapbroy33>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0
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).
On 31.10.2014 16:14, Peter Lammich wrote:
There is something even more weird going on:
imports Main begin
datatype bar = foo
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:
Moreover, in the isabelle/jedit text area, the syntax highlighting is
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.
On Fr, 2014-10-31 at 15:50 +0100, Peter Lammich wrote:
Referring to Isabelle-2014
Hi, I recently encountered the following (strange) behaviour:
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!?
This archive was generated by a fusion of
Pipermail (Mailman edition) and