- Variables in axioms need to be quantified! Some papers on EML don't do this for the sake of readability, but the official definition of EML requires it so that's what the implementation requires.
- Quantification is written
**Forall x => exp**and**Exists x => exp**(and**Exists_unique x => exp**), with capitalized**Forall**and**Exists**. Papers on Extended ML use lower-case**forall**and**exists**but in the implementation there is a conflict with library functions**List.exists**and**Listpair.exists**. - Use
**Forall (x,y) => exp**or**Forall x => Forall y => exp**rather than**Forall x,y => exp**, and similarly for**Exists**. - Use
**==**(EML logical equality, with type**'a * 'a -> bool**) rather than**=**(ML computational equality, with type**''a * ''a -> bool**). The two kinds of equality coincide on types like**bool**and**int**where they are both defined. The negation of**==**is**=/=**. - Put a space between
**?**and**:**when writing things like**fun f(x:int) = ? :int**. The definition of identifiers in ML says that**?:**is an identifier rather than**?**followed by**:**. - Don't use the variable
**o**. This is ML function composition and is declared as infix, which leads to confusing error messages. To cancel the infix status of**o**if you do use it as a variable, specifications should be preceded with**nonfix o**.

Don Sannella. Please mail me if you have any comments on this page. Last modified: Tue Sep 6 12:27:45 BST 2005