mirror of https://github.com/nmvdw/HITs-Examples
22 lines
447 B
Markdown
22 lines
447 B
Markdown
# HITs-Coq
|
|
|
|
Needed: https://github.com/HoTT/HoTT
|
|
|
|
The only part of the project that is buildable is the `FiniteSets` library.
|
|
|
|
# Building
|
|
|
|
Before proceeding make sure that you have [hoqc](https://github.com/HoTT/HoTT) installed.
|
|
|
|
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
|
|
```
|