Good eye. It was accidentally omitted from the document. It is defined as:
WhereClause ::= "where" Expr
Rustan
PS. The "This is Boogie 2" manual also talks about "finite" types. That was the initial design, but the "finite" keyword is neither needed nor allowed. That is, you can declare a finite type without that keyword (but all types do need to
be nonempty).
