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

Пакет: agda (2.5.4.1-3)

Ссылки для agda

Screenshot

Ресурсы Debian:

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

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

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

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

функциональный язык программирования с зависимыми типами

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

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

Метапакет, предоставляющий Agda-режим для Emacs, исполняемые файлы, стандартные библиотеки и документацию.

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

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

Загрузка agda

Загрузить для всех доступных архитектур
Архитектура Размер пакета В установленном виде Файлы
all 115,3 Кб122,0 Кб [список файлов]