[isabelle-dev] [isabelle] Confusing behavior of a paired set comprehension
makarius at sketis.net
Wed Apr 4 12:53:21 CEST 2012
On Wed, 4 Apr 2012, Tobias Nipkow wrote:
> Am 04/04/2012 11:48, schrieb Tjark Weber:
>> Adhering to the principle of least astonishment, I suspect an error
>> message (or at least a warning) would be more helpful.
> Isabelle's well-tried principle of least astonishment is not to give too
> many helpful error messages or warnings ;-)
> Actually, in this case it is not so easy to produce an error message
> because the patterns are translated away with translations and the
> resulting lambda's are perfectly legal.
Yes, things like %x x x x. x and fix x fix x fix x have "x = x" are
perfectly legal and behave quite uniformly for many years, i.e. with
little surprise to people who have got acquainted with Isabelle scoping
To make things even more simple for beginners, the Prover IDE markup
protocol already indicates the internal scopes in the source text. E.g.
when using CONTROL/COMMAND with mouse clicks, one can explore the internal
bindings. It is only a small addition to the display engine to make
variable scopes immediately visible in the source text, like Netbeans
would do for Java for example when the user moves or hovers over the text.
In contrast, lots of warning messages are old-school TTY technology, and
in Proof General the channel for that gets easily overloaded so that the
user is switching into SPAM mode.
More information about the isabelle-dev