-
Make TheoryEncoding.hs use lots of records.
-
Clean Convert.hs and avoid the use of tuples where data types should exist.
-
Update the documentation to reflect all the terminology changes and the added "local declarations".
-
In general, clean all the code.
-
Implement the defaulting as a theory.