Package: wnpp Severity: wishlist Owner: Iain Lane <la...@ubuntu.com> * Package name : agda-stdlib Version : unreleased Upstream Author : Nils Anders Danielsson <n...@cs.nott.ac.uk> * URL : http://wiki.portal.chalmers.se/agda/agda.php?n=Libraries.StandardLibrary * License : MIT/X Programming Lang: Agda Description : standard library for Agda - a dependently typed functional programming language and proof assistant
Agda is a dependently typed functional programming language: It has inductive families, which are like Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code). .. Agda is a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Lf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL. .. This package contains the standard library for Agda, which provides some modules for common programming- and proof-structuring idioms. Modules are included for algebra, category theory, coinduction, data types, the foreign function interface, induction, IO, relations, and sized types. -- System Information: Debian Release: 5.0 APT prefers jaunty-updates APT policy: (500, 'jaunty-updates'), (500, 'jaunty-security'), (500, 'jaunty-backports'), (500, 'jaunty') Architecture: i386 (i686) This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org