diff options
| -rw-r--r-- | README.md | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/README.md b/README.md new file mode 100644 index 0000000..4c2ae38 --- /dev/null +++ b/README.md @@ -0,0 +1,16 @@ +# Isabelle/HoTT +An experimental implementation of HoTT in Isabelle/Pure + +## Installation +Clone the contents of this repository into `<Isabelle root directory>/src/HoTT`. + +## Usage +Set Isabelle's prover to Pure in the Theories panel, and import `HoTT`. + +## About and Collaboration +Collaborators welcome! +I've been working on this library as part of my Masters project, and there are very many improvements and developments that have yet to be implemented. +If you're interested in working together on any part of this do drop me a line! + +## License +MIT |