Chapter 3, End of Introduction to Section 2

The form of quantification in FMSL is common to that of typed predicate logic. The general format of universal quantification is the following: 

forall (x:t) predicate

This is read "for all values x of type t, predicate is true" where x must appear somewhere in predicate.

There are also two extended forms of forall, shown in Table 3.X.



Extended Form Reading Equivalent To
forall (x:t | p1) p2 For all x of type t, such that p1 is true, p2 is true. forall (x:t) if p1 then p2
forall (x in l) p For all x in l, p is true. forall (x:basetype(l)) if x in l then p

Table 3.X: Extended forms of universal quantification




Existential quantification has three comparable forms: 
exists (x:t) predicate


exists (x:t | predicate1) predicate2


exists (x in l) predicate