Package: agda-stdlib (0.17-1)

[ Source: agda-stdlib  ]

Standardbibliotek for Agda

Agda er et afhængighedsindtastet funktionelt programmeringssprog: Det har induktive familier, som fungerer som Haskells GADT'er, men de kan indekseres af værdier og ikke kun af typer. Programmet har også parameteropsatte moduler, mixfix-operatører, Unicodetegn og en interaktiv grænseflade for Emacs (indtastningskontrollen kan hjælpe med udvikling af din kode).

Agda er også en bevisassistent: Programmet er et interaktivt system for skrivning og kontrol af beviser. Agda er baseret på intuitionistisk typeteori, et fundamentsystem for konstruktiv matematik udviklet af den svenske logiker Per Martin-Löf. Programmet har mange ligheder med andre bevisassistenter baseret på afhængighedstyper, såsom Coq, Epigram og NuPRL.

Standardbiblioteket for Agda indeholder moduler for mange gængse datastrukturer og bevismønstre. Tilbudte moduler inkluderer:

 - Algebra: Specifikation og årsagssammenhæng vedrørende algebraiske
            strukturer
 - Category: Brug af idiomer fra kategoriteori til strukturfunktionelle
             programmer
 - Coinduction: Understøttelse for programmeringsinduktion
 - Data: Datatyper og egenskaber om datatyper
 - Foreign: Relaterer til foreign function-grænsefladen
 - Induction: Et generelt rammeværktøj for induktion
 - IO: Input/output relaterede funktioner
 - Level: Universeniveauer
 - Relations: Egenskaber for og beviser omkring relationer
 - Size: Størrelser brugt af mekanismen for størrelsestyper

Denne pakke indeholder det fuldstændige bibliotek.

Tags: Role: Shared Library

Other Packages Related to agda-stdlib

• dep: libghc-agda-dev (<< 2.5.5~)

  Afhængighedsindtastet funktionelt programmeringssprog

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

• enh: elpa-agda2-mode

  Afhængighedsindtastet funktionelt programmeringssprog - tilstand for emacs

Download agda-stdlib

Download for all available architectures

Architecture	Package Size	Installed Size	Files
all	32,247.9 kB	43,615.0 kB	[list of files]