История изменений
Исправление mix_mix, (текущая версия) :
А где-то кто-то объяснял, зачем делать язык с HoTT?
Чтобы можно было заимплементить как минимум всё то, что написано в их книге, очевидно же. Coq слишком ограничен.
Да и вообще, при чем HoTT к инфоматике?
Как теория типов относится к информатике? Лол. Почитай хотя бы введение что ли: http://hottheory.files.wordpress.com/2013/03/hott-a4-611-ga1a258c.pdf
Исходная версия mix_mix, :
Чтобы можно было заимплементить как минимум всё то, что написано в их книге, очевидно же. Coq слишком ограничен.