Paket: agda (2.6.4.3-1)

[ Quellcode: agda  ]

Abhängig typisierte, funktionale Programmiersprache

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 Metapaket liefert den Emacs-Modus, die ausführbare Anwendung, die Standardbibliothek und die Dokumentation für Agda.

Markierungen: Rolle: Meta-Paket

Andere Pakete mit Bezug zu agda

• dep: agda-bin

  Befehlszeilenschnittstelle zu Agda

• dep: agda-stdlib

  Standardbibliothek für Agda

• dep: agda-stdlib-doc

  Standardbibliothek für Agda - Dokumentation

• dep: elpa-agda2-mode

  Abhängig typisierte, funktionale Programmiersprache - Emacs-Modus

• dep: libghc-agda-dev

  Abhängig typisierte, funktionale Programmiersprache

agda herunterladen

Download für alle verfügbaren Architekturen

Architektur	Paketgröße	Größe (installiert)	Dateien
all	11,9 kB	20,0 kB	[Liste der Dateien]