diff options
| author | Josh Chen | 2018-09-18 11:45:22 +0200 |
|---|---|---|
| committer | GitHub | 2018-09-18 11:45:22 +0200 |
| commit | 78f5c8ed483f8c52e902b0c6eb6beb359b5df19c (patch) | |
| tree | d7abc1117ef43f668b9baafcec3dd0eeaadff0cb /README.md | |
| parent | 8295956b656dcfda6d3ec56b96d3d4630ec05d5c (diff) | |
Update README.md
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -2,6 +2,12 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in the interactive theorem prover [Isabelle](https://isabelle.in.tum.de/). +### Usage + +The default entry point for the logic is `HoTT`, which loads everything else. + +You can also load theories selectively, in this case,`HoTT_Base` is required and `HoTT_Methods` is helpful. + ### License GNU LGPLv3 |