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

>>> Подробности

Linux.org.ru прочитано 16035 раз