Re: [isabelle] Case-combinator allows qualified names for bound variables
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:
> 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!?
This archive was generated by a fusion of
Pipermail (Mailman edition) and