aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-07-09 12:58:13 +0200
committerJosh Chen2020-07-09 12:58:13 +0200
commitfc9ba2141aefa685bacc47a9c2eab2cc718d8620 (patch)
tree0f7388e35704f4dbcc537d75e325b182685d282f
parent07c51b1801bd701bef61cedd571a944d9bd37e8b (diff)
caveat
-rw-r--r--README.md2
1 files changed, 2 insertions, 0 deletions
diff --git a/README.md b/README.md
index 6bf78bb..6686e0b 100644
--- a/README.md
+++ b/README.md
@@ -7,6 +7,8 @@ Work is slowly ongoing to develop the logic into a fully-featured framework in w
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.
+**Caveat prover**: *This project is under active experimentation and is not yet guaranteed fit for any particular purpose.*
+
### Usage
Isabelle/HoTT is compatible with Isabelle2020.