Re: Quantified Expressions: "some"

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:puezn7v9naom.1nrc5rh8wzm7p.dlg@40tude.net...
> On Wed, 17 Nov 2010 17:14:27 +0100, J-P. Rosen wrote:
...
>> Actually, It's been decided recently to change "|" to "=>", so it will 
>> read:
>> ( for all X in 1 | 3..5 | F'Range => P(X) )
>
> Not much better: "=>" means "implies." P is neither implied nor selected.
> Actually it is antecedent, on the left side. IF kind of X, such that P(X)
> AND X in the set, THEN something [ ELSE something ].

"=>" is what SPARK uses.

I personally agreed with you and voted for neither. But I was the only one.

                            Randy.