Пакунок: agda (2.5.4.1-3)
Links for agda
Debian Resources:
Download Source Package agda:
Maintainer:
External Resources:
- Homepage [wiki.portal.chalmers.se]
Similar packages:
Функціональна мова програмування з залежними типами
Agda є функціональною мовою програмування з залежними типами. У ній є індуктивні сімейства, які схожі на GADT з Haskell, але вони можуть бути індексовані за значеннями, а не просто за типами. Також у ній є модулі з підтримкою параметризації, міксфіксні оператори, символи Unicode та інтерактивний інтерфейс Emacs (програма перевірки типів може допомогти в розробці Вашого коду).
Також Agda є інтерактивним засобом доведення теорем. Вона є інтерактивною системою запису та перевірки доказів. Agda заснована на інтуїціоністській теорії типів, базовій системі конструктивної математики, розробленої шведським логіком Пером Мартіном-Лефом. Agda в де чому схожа з іншими інтерактивними засобами доведення теорем, заснованими на залежних типах, такими як Coq, Epigram і NuPRL.
Це збірний пакунок, що надає Agda-режим для Emacs, виконувані файли, стандартні бібліотеки та документацію.
Інші пакунки пов'язані з agda
|
|
|
|
-
- dep: agda-bin
- commandline interface to Agda
-
- dep: agda-stdlib
- standard library for Agda
-
- dep: agda-stdlib-doc
- standard library for Agda — documentation
-
- dep: elpa-agda2-mode
- dependently typed functional programming language — emacs mode
-
- dep: libghc-agda-dev
- Функціональна мова програмування з залежними типами
Завантажити agda
| Архітектура | Розмір пакунка | Розмір після встановлення | Файли |
|---|---|---|---|
| all | 115.3 kB | 122.0 kB | [список файлів] |