diff options
| author | Josh Chen | 2018-08-17 16:25:38 +0200 |
|---|---|---|
| committer | GitHub | 2018-08-17 16:25:38 +0200 |
| commit | 090a3317f60e6fdf50ea59d78fb6de008b34f454 (patch) | |
| tree | 03095e42a9f5630670cc8dbeb0e9787081200199 | |
| parent | 5cefd4e82dc9c298074ffa8a4e0240786bdf8fc6 (diff) | |
Create README.md
| -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 |