Re: [isabelle] Confusing behavior of a paired set comprehension



In case it's not obvious, you probably want something like "ident S =
{(x,y). x \in S \and (x = y)}".

On Wed, Apr 4, 2012 at 10:11 AM, Giuliano Losa <giuliano.losa at epfl.ch>wrote:

> Hello,
> the following definition is interpreted in a confusing way:
>
> def ident :: "'a set => ('a \times 'a) set"
> where "ident S = {(x,x) . x \in S}"
>
> the command "thm ident_def" yields
> ident ?S \<equiv> {(xa, x). x \<in> ?S}
>
> Should this be considered as a bug?
>
> Giuliano
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.