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



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.