- Stanford University Centaur Lab
- https://leni.sh
-
Director of NorCal Hakkero Factory No. 1
- Joined on
2023-08-21
refactor: Cleanup the congruence tactics
feat: Elementarized tactics with motives, congruence, and absurdity
Expose the
String.toName
interface
feat: Handling of universe level names in elab
Unclear error message
We likely have to add proper explicit handling of universe levels. This has been the elephant in the room for a year. The downside is that the solver would have to be aware of it.