все параметры
[  buster  ] [  bullseye  ] [  bookworm  ] [  trixie  ] [  sid  ]
[ Источник:  ]

Пакет: agda-bin (2.6.3-1) [debports]

Ссылки для agda-bin

Screenshot

Ресурсы Debian:

Исходный код :

Не найден

Сопровождающие:

Внешние ресурсы:

Подобные пакеты:

интерфейс командной строки для Agda

Agda является функциональным языком программирования с зависимыми типами. В ней имеются индуктивные семейства, которые похожи на GADT из Haskell, но они могут быть индексированы по значениями, а не просто по типам. Также в ней имеются модули с поддержкой параметризации, миксфиксные операторы, символы Unicode и интерактивный интерфейс Emacs (программа проверки типов может помочь в разработке вашего кода).

Также Agda является интерактивным средством доказательства теорем. Она является интерактивной системой записи и проверки доказательств. Agda основана на интуиционистской теории типов, базовой системе конструктивной математики, разработанной шведским логиком Пэром Мартином-Лёфом. Agda во многом схожа с другими интерактивными средствами доказательства теорем, основанными на зависимых типах, такими как Coq, Epigram и NuPRL.

Пакет предоставляет программу командной строки для проверки типов и компиляции программ на Agda. Также программа может создавать HTML-файлы с ссылками и подсветкой из исходного текста на Agda.

Другие пакеты, относящиеся к agda-bin

  • зависимости
  • рекомендации
  • предложения
  • enhances

Загрузка agda-bin

Загрузить для всех доступных архитектур
Архитектура Размер пакета В установленном виде Файлы
alpha (неофициальный перенос) 17 254,1 Кб169 046,0 Кб [список файлов]