Translator state should be stored as per-theory deltas (at least for load/save)
Open
enhancement
translator
- Dominant language
- Standard ML
- Stars
- 1.2k
- Forks
- 104
- Avg merge
- 2d 21h
- Merged PRs (30d)
- 16
Description
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.
Contributor guide
No contributing guide indexed for this repository
Assessment
This issue has not been assessed yet.