<sort> ::= <simple-sort> | <compound-sort> <simple-sort> ::= <simpleId> <compound-sort> ::= <simpleId> "[" <sort>+, "]"
Nat Set[Nat] Map[Set[A],A]
All sorts other than Bool must be declared in a declare sorts command. Except for Bool and bool, which denote the same sort, case is significant in sort identifiers. Thus Nat and nat are different sorts.
Since distinct sorts represent disjoint sets of objects, users who want to consider one ``sort'' (e.g., Nat) as a subset of another (e.g., Int) must resort to one of two devices. They can define the larger as a sort and the smaller by means of a unary predicate (e.g., isNat:Int->Bool). Alternatively, they can define both as sorts and introduce a mapping from one into the other (e.g., asInt:Nat->Int).