2017-01-02 13:07:50 +01:00
|
|
|
# HITs-Coq
|
|
|
|
|
|
|
|
|
|
Needed: https://github.com/HoTT/HoTT
|
2017-01-02 13:43:42 +01:00
|
|
|
|
2017-10-11 13:37:48 +02:00
|
|
|
The Finite Sets library of the 'Finite Sets in Homotopy Type Theory' is in the directory 'Finite Sets'.
|
|
|
|
|
|
2017-08-24 16:53:58 +02:00
|
|
|
The only part of the project that is buildable is the `FiniteSets` library.
|
2017-05-18 17:46:00 +02:00
|
|
|
|
|
|
|
|
# Building
|
|
|
|
|
|
2017-08-24 16:53:58 +02:00
|
|
|
Before proceeding make sure that you have [hoqc](https://github.com/HoTT/HoTT) installed.
|
2017-05-18 17:46:00 +02:00
|
|
|
|
2017-08-24 16:53:58 +02:00
|
|
|
1. Build the `HitTactics` library in `prelude`.
|
|
|
|
|
```
|
|
|
|
|
cd prelude
|
|
|
|
|
hoqc HitTactics
|
|
|
|
|
```
|
|
|
|
|
2. Generate the Makefile and build the `FiniteSets` library
|
|
|
|
|
```
|
|
|
|
|
cd ../FiniteSets
|
|
|
|
|
coq_makefile -f _CoqProject -o Makefile
|
|
|
|
|
make
|
|
|
|
|
```
|
