[isabelle-dev] Highlighting of locale variables
noschinl at in.tum.de
Fri Apr 12 15:40:08 CEST 2013
On 12.04.2013 15:24, Makarius wrote:
> On Fri, 12 Apr 2013, Lars Noschinski wrote:
>> Rationale: In the locale context, these locale variables are morally
>> constants. Somebody suggested to highlight locale variables like
>> constants, but personally I'd prefer a highlighting similar to
>> variables obtained or fixed in a proof (maybe a non-bold orange?).
> Can you point to situations where this is still treated differently?
> Such incidents are mostly coming from the depths of time, as Larry
> usually calls this.
I was referring to variable fixed by a locale. In the example below, "F"
is always rendered like a free variable (i.e. blue); although it's scope
is not the lemma, but the locale.
locale dummy = fixes F :: 'a
lemma "P F"
> There are certain intermediate states, like undeclared frees that are
> implicitly fixed by the system infrastructure via "auto fix", but that
> is slightly different.
An oddity related to this is the let command. In the example below, "a"
is rendered as an undeclared free. This feels wrong as writing such a
statement seems perfectly fine, because constants and variables on the
left hand side are generalized anyway.
let "?X a" = "1 + a"
More information about the isabelle-dev