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



On Thu, 2012-04-05 at 11:25 +0200, Brian Huffman wrote:
> Isabelle's treatment of bound variables is perfectly consistent with
> mainstream functional programming languages like Haskell or ML:
> Function abstractions may shadow existing names.
> 
> (ghci)
> Prelude> :t \x -> \x -> x
> \x -> \x -> x :: t -> t1 -> t1
> 
> (polyml)
> fn x => fn x => x
> val it = fn: 'a -> 'b -> 'b

True, but the original example was "ident S = {(x,x) . x \in S}". Hence
I believe the following behavior to be more relevant:

(polyml)
> fn (x,x) => x;
Error-x has already been bound in this match Found near fn (x, x) => x
Static Errors

Best regards,
Tjark







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