Пакет: elpa-agda2-mode (2.5.4.1-3)

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

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

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

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

Пакет содержит интерактивный режим разработки emacs для Agda. Этот режим является предпочтительным способом написания кода на Agda и предлагает такие возможности, как итеративная разработка, уточнение, анализ случаев и так далее.

Другие пакеты, относящиеся к elpa-agda2-mode

• dep: agda-bin (<< 2.5.4.1-3.1~)

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

  dep: agda-bin (>= 2.5.4.1-3)

• dep: emacsen-common

  общие средства для всех пакетов emacs

• dep: libghc-agda-dev (<< 2.5.4.1-3.1~)

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

  dep: libghc-agda-dev (>= 2.5.4.1-3)

• rec: emacs (>= 46.0)

  редактор GNU Emacs (метапакет)
  также виртуальный пакет, предоставляемый emacs-gtk, emacs-lucid, emacs-nox

• enh: emacs

  редактор GNU Emacs (метапакет)
  также виртуальный пакет, предоставляемый emacs-gtk, emacs-lucid, emacs-nox

• enh: emacs24

  GNU Emacs transitional package to emacs-gtk

Загрузка elpa-agda2-mode

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

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