Установка:

Для установки 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.

Список зависимостей:

  • libc6

  • libffi6

  • libgmp10

  • libtinfo5

    общая библиотека terminfo низкого уровня для обработки терминала

  • zlib1g

    библиотека сжатия - время выполнения