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