| |||
|
|
Изначально она заточена под теорию типов и проверку программ, гомотопии и алгем идут приятным бесплатным бонусом. Поскольку теория множеств в ней легко выразима, препятствие одно: людям лень писать код. Публиковать теоремы же приятнее, чем верифицировать их. Добавить комментарий: |
|||