Iterator

iterator = names in generator {, names in generator} [filter]
filter = (||where) condition
names = name {[,] name}
generator = expression | name in generator

Iterators appear in for loops, set constructors, list constructors and the forall (universal) and forsome (existential) quantifiers. Iterators serve to bind a succession of values to one or more names. The names appearing in an iterator a local to a name space associated with the construct containing the iterator.

Iterators are usually quite simple, consisting of a name and an expression resulting a collection of values, for example:

  k in [1..10]

The optional filter condition makes it possible to bind selectively, for example, to bind only values greater than 10, use:

  k in S | k > 10

When iterating through a collection of lists, individual names can be bound to the components of each list, for example:

  i, s in {[1, `one'] [2, `two']}

Alternatively, the iterator can be used to flatten a collection of lists by using a nested generator expression, for example:

  i in j in [[1 2] [3 4]]

which is the same as

  i, j in [[1 [1 2]] [2 [1 2]] [3 [3 4]] [4 [3 4]]

Iterators can also traverse multiple collections, without the need to construct explicit Cartesian Products, for example

  i in [1 2], j in [`a' `b']

which is the same as

 i, j in [[1 `a'] [1 `b'] [2 `a'] [2 `b']]

Note that the second generator expression is re-evaluated for every bound value of the first expression. For example

 i in [1..3], j in [1..i] | odd(i)

is the same as

  i, j in [[1 1] [3 1] [3 2] [3 2]]