Re: [isabelle] Case-combinator allows qualified names for bound variables
- To: Peter Lammich <lammich at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>
- 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:53:59 +0100
- In-reply-to: <1414767041.30420.5.camel@lapbroy33>
- References: <1414767041.30420.5.camel@lapbroy33>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0
On 31.10.2014 15:50, Peter Lammich wrote:
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.
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!?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and