A type that encapsulates an atom of text. Lists of characters
make up strings.
datatype character
| ← ordered set | ideal • library • elements • character | string → |
| ← ordered set | ideal • library • elements • character | string → |