|HoTT HITs||Andrej Bauer||3/6/13 12:58 PM|
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 checkout stable
Then rebuild Coq, probably as follows:
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:
I will let someone else explain how the hits are implemented.
With kind regards,