Some sort of visual indication that the same variable is being bound twice might be useful, though that sort of thing is easy to overlook. Larry
On 22 Mar 2013, at 13:15, Tjark Weber <[email protected]> wrote: > On Fri, 2013-03-22 at 13:25 +0100, Makarius wrote: >> On Fri, 22 Mar 2013, Andreas Lochbihler wrote: >>> "{(x, y). P}" is pretty syntax for >>> "Collect (prod_case (%x y. P))", so in your case, you get >>> "Collect (prod_case (%v v. v : {''a'', ''b''}))" >>> See how the second v in %v v. ... hides the former. >>> >>> There is no warning because it is perfectly normal to rebind a variable >>> name in a lambda abstraction. >> >> 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). But it is similar to established mathematical notation, so > users might (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 > > Best, > Tjark > > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
