Floor1
Floor1 is a super basic proof assistant, implemented using PHOAS-like approach as an experiment.
Floor1 does not support any elegant features currently, nor is there a plan to add such. The only possibly reasonable application of Floor1 is pedagogical practice, but even that won't provide high-quality experience until all main functionalities are done. For more information, check the following TODO list.
TODO list
- Backward reasoning (WIP)
- Theorem parser
- Command parser
- Text user interface
- Forward reasoning
- Emacs mode
- Proof term generation
- Proof search
- Data types
- Module system