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
begin
lemma "P F"
oops
-----------
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.
-----------
notepad begin
let "?X a" = "1 + a"
end
-----------
-- Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
