Coq 8.9
Состоялся релиз Coq 8.9. Его разработка заняла 7 месяцев с момента выпуска Coq 8.8. Этот релиз является результатом ≈2000 коммитов и ≈500 pull request«ов.
Coq — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования с зависимыми типами.
Особенностью Coq является широкое использование тактик для построения доказательств, в отличие от таких систем, как Agda или Idris.
Основные изменения в этой версии:
- Поддержка взаимно рекурсивных record«ов (Pierre-Marie Pédrot).
- Добавлена команда
Numeral Notationдля перегрузки десятичных чисел сторонними типами (Daniel de Rauglaudre, Pierre Letouzey и Jason Gross). {теперь поддерживает именованные цели, например[x]:{(Théo Zimmermann).- Удалены команды
Arguments ScopeиImplicit Arguments. coqtopиcoqideтеперь могут подсвечивать разницу в шагах доказательства, используя командуDiffs.- Изменения в стандартной библиотеке: в библиотеках
VectorDef,Ascii,String. - Удалена утилита
gallina. - Многочисленные исправления в новой документации, основанной на Sphinx.
>>> Подробности
