Ubuntu
agda package

agda 2.2.10-4build1 source package in Ubuntu

agda (2.2.10-4build1) precise; urgency=low

  * Rebuild for new GHC ABIs.
 -- Colin Watson <email address hidden>   Mon, 14 Nov 2011 08:42:48 +0000

Series	Pocket	Published	Component	Section

File	Size	SHA-256 Checksum
agda_2.2.10.orig.tar.gz	505.6 KiB	5cd3b69a744b86b74344b790350d8a6f2b62f206f5a53a9cfad22cc3ca3309ae
agda_2.2.10-4build1.debian.tar.gz	7.9 KiB	9eed2b214be97b5c21bdbd054cdf34714ac6794c0e8d8cbe802df52a2271290b
agda_2.2.10-4build1.dsc	3.2 KiB	aabcca811e91e191c7acbfe4532ebea4e9d181c3b16e053d9bfa4845b939144c

agda: dependently typed functional programming language: 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 also 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-Löf. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
.
This is a meta package which provides Agda's emacs mode, executable, standard
library and its documentation.

agda-mode: dependently typed functional programming language — emacs mode: 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 also 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-Löf. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
.
This package contains the emacs interactive development mode for Agda. This
mode is the preferred way to write Agda code, and offers features such as
iterative development, refinement, case analysis and so on.

libghc-agda-dev: dependently typed functional programming language - development libraries: 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 also 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-Löf. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
.
This package contains the normal library files.

libghc-agda-doc: dependently typed functional programming language - documentation: 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 also 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-Löf. It has many similarities with other proof assistants based on
dependent types, such as Coq, Epigram and NuPRL.
.
This package contains the documentation files.