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



No, a feature. Patterns may not contain repeated variables.

Tobias

Am 04/04/2012 11:11, schrieb Giuliano Losa:
> 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.