- Read An Efficient Unification Algorithm, and skim through other papers solving various kinds of unification problems
- Update the documentation
- Enable GitHub Actions and set up a Maven repository. Released
0.1- The framework is (internally) being tested for usability by other users
- Implement some of the remaining rules that rely on higher order symbols
- Create a simple stateful proof mode datastructure
- It is now possible to lift symbols, terms and formulas from the kernel to the front
- In particular set theory
- Goals can be reordered and tactics can be unapplied
- General refactoring
- lampepfl/dotty#14818, lampepfl/dotty#14834