Установка:
Для установки agda-bin в Ubuntu / Linux Mint / Debian, введите в Терминал:
sudo apt update
sudo apt install agda-bin
Подробная информация о пакете:
интерфейс командной строки для Agda
Agda — это функционально-зависимый язык программирования: он имеет индуктивные семейства, которые похожи на GADT Haskell, но их можно индексировать значениями, а не только типами. Он также имеет параметризованные модули, операторы mixfix, символы Unicode и интерактивный интерфейс Emacs (средство проверки типов может помочь в разработке вашего кода).
Agda также является помощником по проверке: это интерактивная система для написания и проверки доказательств. Агда основана на теории интуиционистского типа, основополагающей системе конструктивной математики, разработанной шведским логиком Пер Мартином-Лёфом. Он имеет много общего с другими помощниками по коррекциям на основе зависимых типов, таких как Coq, Epigram и NuPRL.
Этот пакет предоставляет программу командной строки для проверки типов и компиляции программ Agda. Программа также может генерировать гиперссылки, выделенные HTML-файлы из источников Agda.