foreach i,j:SomeSet do _

In order for the foreach to only define i and j in the body a defines in must be used.
In order to both define i and j a pattern match in NaBL must be use to match the ATerms of those, not the surrounding Foreach ATerm.

Preferred solution: support for lists:

Foreach(name*,expr,body): defines Variable name of type e-ty in body where e has type e-ty

Quantifiation makes it is even more interesting

some n1,n2:Name, all a:Address | Exp

there are two nested lists now. A syntax could look something like

Quantifier(CommaList(name*,expr)*,body): defines Variable name of type e-ty in body where e has type e-ty

Possible workaround: make these definitions and let them scope variables. But that would not completely solve it because then one can self-reference a defined variable.

Submitted by Daco Harkes on 30 January 2015 at 16:26