diff options
| author | Josh Chen | 2020-07-09 12:58:13 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-09 12:58:13 +0200 |
| commit | fc9ba2141aefa685bacc47a9c2eab2cc718d8620 (patch) | |
| tree | 0f7388e35704f4dbcc537d75e325b182685d282f | |
| parent | 07c51b1801bd701bef61cedd571a944d9bd37e8b (diff) | |
caveat
| -rw-r--r-- | README.md | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -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. |