Состоялся релиз 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.
>>> Подробности
