Re: Quantified Expressions: "some"

[AdaMagica <christoph.grein@eurocopter.com>]

On 18 Nov., 09:47, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Wed, 17 Nov 2010 19:12:53 -0600, Randy Brukardt wrote:
> > "Dmitry A. Kazakov" <mail...@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.
>
> At least they could use "when" instead of "=>".

( for all X in 1 | 3..5 | F'Range when P(X) ) ?????

That's nonsense, it's the other way round (compare exit L when ...
case X is when ...). If we are dreaming up syntax:

Use a colon or double colon:

( for all X in 1 | 3..5 | F'Range :: P(X) )