Closed inexxt closed 3 years ago
TODOs are refactored into two kinds:
TODO
TODO!
TODO-
We can now just grep "TODO\!" and if we fill all of them, the proof is finished.
grep "TODO\!"
The convention is that all new TODOs are TODO!, and only after proving it some other way, it can be turned into TODO-.
I didn't touch the FSMG stuff, which uses normal TODO as before.
TODOs are refactored into two kinds:TODO!- essential onesTODO-- non-essential onesWe can now just
grep "TODO\!"and if we fill all of them, the proof is finished.The convention is that all new
TODOs areTODO!, and only after proving it some other way, it can be turned intoTODO-.I didn't touch the FSMG stuff, which uses normal
TODOas before.