Paket: elpa-agda2-mode (2.6.4.3-1)

[ Quellcode: agda  ]

Abhängig typisierte, funktionale Programmiersprache - Emacs-Modus

Agda ist eine abhängig typisierte, funktionale Programmiersprache: Sie besitzt induktive Familien, die wie Haskells GADTs sind, jedoch mit Werten und nicht nur mit Typen indiziert werden können. Zusätzlich besitzt sie parametrisierte Module, mixfix-Operatoren, Unicode-Kodierung und eine interaktive Emacs-Schnittstelle (die Typüberprüfung kann bei der Codeentwicklung hilfreich sein).

Agda ist auch ein Beweisassistent, ein interaktives System zum Schreiben und Überprüfen von Beweisen. Agda basiert auf der intuitionistischen Typentheorie, einem grundlegenden System für konstruktive Mathematik, entwickelt vom schwedischen Logiker Per Martin-Löf. Es ähnelt anderen Beweisassistenten, die auf abhängigen Typen basieren, wie Coq, Epigram und NuPRL.

Dieses Paket enthält den Emacs-Modus zur Entwicklung mit Agda. Dieser Modus ist die bevorzugte Art Agda-Code zu schreiben und bietet Funktionen an, wie iterative Entwicklung, Verbesserung, Fallanalysen usw.

Andere Pakete mit Bezug zu elpa-agda2-mode

• dep: agda-bin (<< 2.6.4.3-1.1~)

  Befehlszeilenschnittstelle zu Agda

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

• dep: dh-elpa-helper

  Hilfspaket für Emacs-Lisp-Erweiterungen

• dep: emacsen-common

  Gemeinsame Funktionen aller Emacs-Varianten

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

  Abhängig typisierte, funktionale Programmiersprache

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

• rec: emacs (>= 46.0)

  Editor GNU Emacs (Metapaket)
  auch ein virtuelles Paket, bereitgestellt durch emacs-gtk, emacs-lucid, emacs-nox, emacs-pgtk

• enh: emacs

  Editor GNU Emacs (Metapaket)
  auch ein virtuelles Paket, bereitgestellt durch emacs-gtk, emacs-lucid, emacs-nox, emacs-pgtk

• enh: emacs24

  Paket nicht verfügbar

elpa-agda2-mode herunterladen

Download für alle verfügbaren Architekturen

Architektur	Paketgröße	Größe (installiert)	Dateien
all	50,1 kB	211,0 kB	[Liste der Dateien]