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



On 31.10.2014 15:50, 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 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




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