aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2019-10-15 23:13:00 +0200
committerGitHub2019-10-15 23:13:00 +0200
commitb815a897c04350f6b2335a15e30844316a5cce9e (patch)
tree8fec941d6dc71bdb40c93c5ded701c75ddfe9504
parentb01b8ee0f3472cb728f09463d0620ac8b8066bcb (diff)
Update README.md
-rw-r--r--README.md1
1 files changed, 1 insertions, 0 deletions
diff --git a/README.md b/README.md
index f254a8a..edc5399 100644
--- a/README.md
+++ b/README.md
@@ -16,6 +16,7 @@ In its current state it is best viewed as a formalization of HoTT within Isabell
Work is slowly ongoing to develop the logic into a fully-featured framework in which one can formulate and prove mathematical statements, in the style of the univalent foundations school.
While Isabelle has provided support for object logics based on Martin-Löf type theory since the beginning, these have largely been ignored in favor of Isabelle/HOL.
Thus this project is also an experiment in creating a viable framework, based on dependent type theory, inside the simple type theoretic foundations of Isabelle/Pure.
+**Update (15 Oct 2019)**: Framework development currently [here](https://github.com/jaycech3n/Isabelle-Spartan).
### License