Package: elpa-agda2-mode (2.6.1-1)

[ 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.6.1-1.1~)

  interfaccia a riga di comando per Agda

  dep: agda-bin (>= 2.6.1-1)

• dep: dh-elpa-helper

  pacchetto ausiliario per estensioni Emacs Lisp

• dep: emacsen-common

  funzionalità comuni per tutti gli emacs

• dep: libghc-agda-dev (<< 2.6.1-1.1~)

  linguaggio di programmazione funzionale tipizzato in modo dipendente

  dep: libghc-agda-dev (>= 2.6.1-1)

• 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

  Package not available

Download elpa-agda2-mode

Download for all available architectures

Architecture	Package Size	Installed Size	Files
all	65.3 kB	220.0 kB	[list of files]