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



 agda, зависимые типы
Ссылка: http://feedproxy.google.com/~r/org/LOR/~3/Lb12wpd9rlk/10554306