cakeml
cakeml copied to clipboard
Translator state should be stored as per-theory deltas (at least for load/save)
Currently, the translator dumps all of its state to "disk" with every export theory, when really, it should just dump the changes (new stuff) to disk and then have the loading of theories incrementally build the whole required state. This would mimic the way things like the stateful simpset is built from per-theory sets of theorems.