Пакет: agda (2.6.2.2-1.1)

[ Источник: agda  ]

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

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

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

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

Теги: Роль: Метапакет

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

• dep: agda-bin

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

• dep: agda-stdlib

  стандартная библиотека для Agda

• dep: agda-stdlib-doc

  стандартная библиотека для Agda

• dep: elpa-agda2-mode

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

• dep: libghc-agda-dev

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

Загрузка agda

Загрузить для всех доступных архитектур

Архитектура	Размер пакета	В установленном виде	Файлы
all	12,0 Кб	20,0 Кб	[список файлов]