Package: elpa-agda2-mode (2.5.4.1-3)

[ Source: agda  ]

linguaggio di programmazione funzionale tipizzato in modo dipendente - modalità Emacs

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 pacchetto contiene la modalità di sviluppo interattivo di Emacs per Agda. Questa modalità è quella preferita per scrivere codice Agda e mette a disposizione funzionalità come lo sviluppo iterativo, raffinamenti, analisi di casi e così via.

Other Packages Related to elpa-agda2-mode

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

  interfaccia a riga di comando per Agda

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

• dep: emacsen-common

  funzionalità comuni per tutti gli emacs

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

  linguaggio di programmazione funzionale tipizzato in modo dipendente

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

• rec: emacs (>= 46.0)

  editor GNU Emacs (metapacchetto)
  also a virtual package provided by emacs-gtk, emacs-lucid, emacs-nox

• enh: emacs

  editor GNU Emacs (metapacchetto)
  also a virtual package provided by emacs-gtk, emacs-lucid, emacs-nox

• enh: emacs24

  pacchetto di transizione a emacs-gtk di GNU Emacs

Download elpa-agda2-mode

Download for all available architectures

Architecture	Package Size	Installed Size	Files
all	151.8 kB	305.0 kB	[list of files]