*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning*From*: Makarius <makarius at sketis.net>*Date*: Fri, 22 Mar 2013 13:25:47 +0100 (CET)*Cc*: "C. Diekmann" <diekmann at in.tum.de>, USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <514C0AC3.8080605@inf.ethz.ch>*References*: <CAGbqCMwbsBO6Gd6rp2nXe8S1i1mraZ8AjHC=38Cn-j_FufH-hA@mail.gmail.com> <514C0AC3.8080605@inf.ethz.ch>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 22 Mar 2013, Andreas Lochbihler wrote:

You want "{(v, v) | v. v : {''a'', ''b''}}". The syntax for setcomprehension is such that you should explicitly mention bound variablesbetween "|" and ".", i.e., v in this case. In some simple cases, thiscan be avoided, and you ran into one of them:"{(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 variablename in a lambda abstraction.

Makarius

**References**:

- Previous by Date: Re: [isabelle] Matching done by the transfer method
- Next by Date: Re: [isabelle] Matching done by the transfer method
- Previous by Thread: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
- Next by Thread: Re: [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
- Cl-isabelle-users March 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list