QuoteRef: shawM8_1976 ;;6 generator for iteration: provides initialization and next functions by extension whose base type is same as iteration variable

QuoteRef: shawM8_1976 ;;7 iteration variable is bound to each value of generator

QuoteRef: shawM8_1976 ;;7 Alphard: for x: gen (y) while predicate (x) do statement both generator and while clauses are optional

QuoteRef: shawM8_1976 ;;8 Alphard: 'first x: gen (y) 'suchthat predicate (x) 'then statement 'else statement

8 ;;Quote: a common use of loops is to search a sequence for the first element that passes a test; needs an exit or goto statement

9 ;;Quote: can define an Alphard form as an extension of another one

QuoteRef: shawM8_1976 ;;13 gives proof techniques for both for and first constructor