Package: agda (2.5.4.1-3)

[ Source: agda  ]

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.

Tags: Role: Metapackage

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

Download for all available architectures

Architecture	Package Size	Installed Size	Files
all	115.3 kB	122.0 kB	[list of files]