Сабж.
Анонс в coq-club:
In case anyone is in the mood to take a break from worrying about the inconsistency of HoTT Coq, here's a quick announcement.
For a few years now, I've been working on a book introducing Coq with an unusual slant, focusing on what I think are the most important techniques to implement and maintain large developments: http://adam.chlipala.net/cpdt/
The book has been available freely online from the start, and I'm pleased to announce that a print version from MIT Press is now available. You can find online ordering links on the page I've referenced.
I'm grateful to MIT Press for agreeing to this experiment where I may continue distributing free versions of the book online.
