Re: [isabelle] Confusing behavior of a paired set comprehension
On Wed, 4 Apr 2012, Jonas Wagner wrote:
No, a feature. Patterns may not contain repeated variables.
+1 vote for "bug".
The fact that Patterns may not contain repeated variables is perfectly fine.
The fact that the first occurrence of a repeated variable is silently
replaced by another variables is not fine.
But that's just the option of an Isabelle Newbie who got his proof wrong
due to a surprising feature ;)
This thread got split over two isabelle mailing lists for unknown reasons,
so I repeat my answer from isabelle-dev here once more:
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 rules.
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.
Jonas, since you are from EPFL you are probably familier with the Scala
scoping, which is often more harsh in forbidding plain nesting of scopes
that would be just fine in the ML, HOL, Haskell tradition. I find the
Scala behaviour quite confusing at times.
Anyway the IDE solution sketched above will make things easier for
beginners without having to reconsider traditions that are established for
decades in certain communities.
This archive was generated by a fusion of
Pipermail (Mailman edition) and