Package: agda (2.6.2.2-1.1)
Links for agda
Debian Resources:
Download Source Package agda:
Maintainer:
External Resources:
- Homepage [wiki.portal.chalmers.se]
Similar packages:
linguaggio di programmazione funzionale tipizzato in modo dipendente
Agda è un linguaggio di programmazione funzionale tipizzato in modo dipendente: ha famiglie induttive che sono simili alle GADT di Haskell, ma possono essere indicizzate in base ai valori e non soltanto ai tipi. Ha anche moduli parametrizzati, operatori mixfix, caratteri Unicode e un'interfaccia Emacs interattiva (il verificatore dei tipi può assistere nella scrittura del codice).
Agda è anche un assistente per dimostrazioni: è un sistema interattivo per scrivere e verificare dimostrazioni. Agda è basato sulla teoria intuizionista dei tipi, un sistema fondante per lo sviluppo della matematica costruttiva creata dal logico svedese Per Martin-Löf. Ha molte similitudini con altri assistenti per dimostrazioni basati su tipi dipendenti, come Coq, Epigram e NuPRL.
Questo è un metapacchetto che fornisce la documentazione, la libreria standard, l'eseguibile, la modalità Emacs di Agda.
Other Packages Related to agda
|
|
|
|
-
- dep: agda-bin
- interfaccia a riga di comando per Agda
-
- dep: agda-stdlib
- libreria standard per Agda
-
- dep: agda-stdlib-doc
- libreria standard per Agda - documentazione
-
- dep: elpa-agda2-mode
- linguaggio di programmazione funzionale tipizzato in modo dipendente - modalità Emacs
-
- dep: libghc-agda-dev
- linguaggio di programmazione funzionale tipizzato in modo dipendente
Download agda
| Architecture | Package Size | Installed Size | Files |
|---|---|---|---|
| all | 12.0 kB | 20.0 kB | [list of files] |