From fc9ba2141aefa685bacc47a9c2eab2cc718d8620 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 9 Jul 2020 12:58:13 +0200 Subject: caveat --- README.md | 2 ++ 1 file changed, 2 insertions(+) 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. -- cgit v1.2.3