- Read The use of machines to assist in rigorous proof (thanks to Rodrigo for the pointer)
- Attempt to implement a meta logic system, where sequents could take either formulas
or other sequents as well
- The implementation of other mechanisms that relied on this foundation turned out to be too complicated and left too many design choices open. Therefore, I decided to leave this idea aside and resume the regular implementation I had started.
- Refactored the front and allow high order functions to work with unification (although we don't expect them to be inferred, yet)
- Rules now support forward proofs as well, without having to implement any additional logic
- lampepfl/dotty#14765