HoTT HITs

Showing 1-1 of 1 messages
HoTT HITs Andrej Bauer 3/6/13 12:58 PM
Dear all,

we have Agda-style higher-inductive types in coq. Thanks to Yves
Bertot, Michael Nahas and Mike Shulman for setting things up. You will
have to recompile Coq to get Yves's changes. If you are an existing
HoTT user, you should

1. Switch to the stable branch of HoTT/coq. From within your copy of HoTT/coq:

   git pull
   git checkout stable

Then rebuild Coq, probably as follows:

   ./configure -local
   make clean
   make coqlight

If you have a dual core or better use insetad 'make -j 2 coqlight'

2. Update your HoTT to get theories/HIT/hit directory, i.e., from your
copy of HoTT/HoTT:

   git pull
   make clean
   make

I will let someone else explain how the hits are implemented.

With kind regards,

Andrej