Вышла Agda 2.4.0
Чистый функциональный язык программирования и система автоматического доказательства Agda обновилась до версии 2.4.0. Новый выпуск содержит солидное число изменений и улучшений, некоторые из которых представлены ниже:
экспериментальная возможность: Varying arity — теперь клозы функции могут иметь различное число аргументов; бекэнд MAlonzo теперь позволяет компилировать неполные программы (т.е. без функции main). Основная цель — написать на Agda лишь часть программы, для которой позднее можно дописать недостающий Haskell-код. Введена новая опция командной строки --compile-no-main; представлено новый модуль Agda.Primitive; экспериментальная возможнось: copatterns (с соответствующей опцией {-# OPTIONS --copatterns #-}); незначительные изменения в синтаксисе; многочисленные улучшения в agda-mode для Emacs. agda, зависимые типы
