Package: agda-stdlib-doc (1.7.3-1)

Standardbibliotek for Agda - dokumentation

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 den hyperhenviste biblioteksdokumentation.

Tags: Software Development: Documentation, Made Of: HTML, Hypertext Markup Language, Role: Documentation

This page is also available in the following languages (How to set the default document language):