On Fri, 22 Mar 2013, Tjark Weber wrote:
I agree that it is perfectly normal, just like term "λx x x. x", and no
warning or error is to be expected.
Clearly, different people have different expectations. "{(v,v). P v}"
is not a lambda abstraction (regardless of how it is represented
internally).
So how about "λ(v. v). v" then?
Anyway, when I've got exposed to this slightly sugared lambda-calculus in
Isabelle for the first time in 1993, I found its simplicity and uniformity
a great relieve, compared to all these adhoc explanations about binders in
informal mathematics. You merely need to learn very few priniciples, and
then you know how it works. Of course, you need to develop a sense what a
binding occurrence of a variable is.
Color schemes in the editor can help to teach people what these principles
of binding and scoping are. In the 1990-ies, black, blue, green variables
were a big thing. Today, it is just a tiny little step to visualize scope
groups in Isabelle/jEdit in a similar way you ee in Netbeans etc. for
Java. (You can already following the implicit hyperlinks in Isabelle2013.)
and, as this thread again shows, do) expect it to denote some subset of
the identity relation. See also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-April/msg00028.html
So I won't have to recycle the old jokes again -- its all there on the
thread from 1 year ago.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
