aboutsummaryrefslogtreecommitdiff
path: root/README.md
diff options
context:
space:
mode:
authorJosh Chen2018-08-17 16:25:38 +0200
committerGitHub2018-08-17 16:25:38 +0200
commit090a3317f60e6fdf50ea59d78fb6de008b34f454 (patch)
tree03095e42a9f5630670cc8dbeb0e9787081200199 /README.md
parent5cefd4e82dc9c298074ffa8a4e0240786bdf8fc6 (diff)
Create README.md
Diffstat (limited to 'README.md')
-rw-r--r--README.md16
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