Ubuntu
agda package

agda 2.4.2.2-4build1 source package in Ubuntu

agda (2.4.2.2-4build1) wily; urgency=medium

  * Rebuild for new GHC ABIs.

 -- Colin Watson <email address hidden>  Sun, 16 Aug 2015 09:51:20 +0100

Series	Pocket	Published	Component	Section

File	Size	SHA-256 Checksum
agda_2.4.2.2.orig.tar.gz	940.7 KiB	2344107654d0cb2a18dcf179ed3ea0f427839e058771ed628da64fbaed55bbc3
agda_2.4.2.2-4build1.debian.tar.xz	8.6 KiB	ef7313b239c0ab9f74f9dc82dd8af309c5e3f09d1343140b53218c0381ec54e4
agda_2.4.2.2-4build1.dsc	3.6 KiB	ddb7c687270db1506b9c2fd84d97ca61f8a740180282166bbe6098c0064833cd

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-bin: No summary available for agda-bin in ubuntu wily.: No description available for agda-bin in ubuntu wily.

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: 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 provides a library for the Haskell programming language.
See http://www.haskell.org/ for more information on Haskell.

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 provides the documentation for a library for the Haskell
programming language.
See http://www.haskell.org/ for more information on Haskell.