jarlg / central-types Goto Github PK

You should be able to build this using Dune with something like:

dune

(coq.theory
 (name CentralTypes) ; can be changed
 (theories HoTT)
 (mode vo) ; no native
 (stdlib no) ; not stldlib
 (flags -noinit -indices-matter))

and a dune-project file like:

(lang dune 3.7)
(using coq 0.7)

Then you can simply drop this project into Coq-HoTT and it will build together, or alternatively have them both in a directory with a dune-workspace file containing (lang dune 3.7).

Soon Dune 3.8 will be released and it will mean you can install the HoTT library using opam and build this repo directly. For now you can build them together.