Пакет: agda-stdlib (1.7.1-1)
Ссылки для agda-stdlib
Ресурсы Debian:
- Сообщения об ошибках
- Developer Information
- Debian журнал изменений
- Файл авторских прав
- Отслеживание заплат Debian
Исходный код agda-stdlib:
Сопровождающие:
Внешние ресурсы:
- Сайт [wiki.portal.chalmers.se]
Подобные пакеты:
стандартная библиотека для Agda
Agda является функциональным языком программирования с зависимыми типами. В ней имеются индуктивные семейства, которые похожи на GADT из Haskell, но они могут быть индексированы по значениями, а не просто по типам. Также в ней имеются модули с поддержкой параметризации, миксфиксные операторы, символы Unicode и интерактивный интерфейс Emacs (программа проверки типов может помочь в разработке вашего кода).
Также Agda является интерактивным средством доказательства теорем. Она является интерактивной системой записи и проверки доказательств. Agda основана на интуиционистской теории типов, базовой системе конструктивной математики, разработанной шведским логиком Пэром Мартином-Лёфом. Agda во многом схожа с другими интерактивными средствами доказательства теорем, основанными на зависимых типах, такими как Coq, Epigram и NuPRL.
Стандартная библиотека Agda содержит модули для многих общих структур данных и шаблонов доказательств. Предоставляемые модули включают:
- Algebra: определение и рассуждение об абстрактных алгебраическихструктурах
- Category: использование идиом из теории категорий для структурированияфункциональных программ
- Coinduction: поддержка коиндуктивного программирования - Data: типы данных и свойства типов данных - Foreign: относящееся к внешнему функциональному интерфейсу - Induction: общая инфраструктура для индукции - IO: функции, связанные с вводом/выводом - Level: уровни Universe - Relations: свойства и доказательства отношений - Size: размеры, используемые механизмом типов с размером
Пакет содержит полную библиотеку.
Другие пакеты, относящиеся к agda-stdlib
|
|
|
|
-
- dep: libghc-agda-dev (<< 2.6.3~)
- функциональный язык программирования с зависимыми типами
- dep: libghc-agda-dev (>= 2.6.2)
-
- enh: elpa-agda2-mode
- функциональный язык программирования с зависимыми типами — режим emacs
Загрузка agda-stdlib
Архитектура | Размер пакета | В установленном виде | Файлы |
---|---|---|---|
all | 97 698,3 Кб | 130 703,0 Кб | [список файлов] |