On Thu, 2006-01-19 at 19:18 -0800, [EMAIL PROTECTED] wrote: . . . > _variables_. The paper argues, btw, for the separation of those senses > and for a new quantifier to mean uniqueness only. In short, when we > write > forall x. forall y. body > then x may well be equal to y (in body). And so, > forall x. forall y. B[x,y] ====> forall z. B[z,z] > OTH, when we write |nabla x. nabla y. body| then x and y are > guaranteed to be different, and so the implication above no longer holds.
OK, I gotta ask: is |nabla x, nabla y. phi(x,y)| logically equivalent to |forall x, forall y. x <> y only-if phi(x,y)|? I use |P only-if Q| for |P materially implies Q|. -- Bill Wood _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
