← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to debian/control

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-z32cspkedler3e2e
Tags: 0.3-1
http://bugs.debian.org/522914
Initial release. (Closes: #522914)

Show diffs side-by-side

added added

removed removed

Lines of Context:
debian/control
 
1
Source: agda-stdlib
 
2
Priority: extra
 
3
Section: libs
 
4
Maintainer: Iain Lane <laney@ubuntu.com>
 
5
Build-Depends: debhelper (>= 7.0.50~),
 
6
               agda-bin (>= 2.2.6),
 
7
               agda-bin (<< 2.2.6.1~),
 
8
               libghc6-agda-dev (>= 2.2.6),
 
9
               libghc6-agda-dev (<< 2.2.6.1~),
 
10
               ghc6,
 
11
               libghc6-filepath-dev,
 
12
               libghc6-filemanip-dev
 
13
Standards-Version: 3.8.4
 
14
Vcs-Browser: http://git.debian.org/?p=collab-maint/agda-stdlib.git
 
15
Vcs-Git: git://git.debian.org/git/collab-maint/agda-stdlib.git
 
16
Homepage: http://wiki.portal.chalmers.se/agda/
 
17
 
 
18
Package: agda-stdlib
 
19
Architecture: any
 
20
Depends: ${misc:Depends}
 
21
Enhances: agda-mode
 
22
Description: a dependently typed functional programming language - standard library
 
23
 Agda is a dependently typed functional programming language: It has inductive
 
24
 families, which are like Haskell's GADTs, but they can be indexed by values and
 
25
 not just types. It also has parameterised modules, mixfix operators, Unicode
 
26
 characters, and an interactive Emacs interface (the type checker can assist in
 
27
 the development of your code).
 
28
 .
 
29
 Agda is also a proof assistant: It is an interactive system for writing and
 
30
 checking proofs. Agda is based on intuitionistic type theory, a foundational
 
31
 system for constructive mathematics developed by the Swedish logician Per
 
32
 Martin-Löf. It has many similarities with other proof assistants based on
 
33
 dependent types, such as Coq, Epigram and NuPRL.
 
34
 .
 
35
 The Agda standard library contains modules for many common data structures and
 
36
 proof patterns. Modules provided include:
 
37
  - Algebra: Specifying and reasoning about abstract algebraic structures
 
38
  - Category: Using idioms from category theory to structure functional programs
 
39
  - Coinduction: Support for programming coindutively
 
40
  - Data: Data types and properties about data types
 
41
  - Foreign: Relating to the foreign function interface
 
42
  - Induction: A general framework for induction
 
43
  - IO: Input/output related functions
 
44
  - Level: Universe levels
 
45
  - Relations: Properties of and proofs about relations
 
46
  - Size: Sizes used by the sized types mechanism
 
47
 .
 
48
 This package contains the complete library.
 
49
 
 
50
Package: agda-stdlib-doc
 
51
Architecture: all
 
52
Section: doc
 
53
Depends: ${misc:Depends}
 
54
Suggests: agda-stdlib
 
55
Description: a dependently typed functional programming language - profiling libraries
 
56
 Agda is a dependently typed functional programming language: It has inductive
 
57
 families, which are like Haskell's GADTs, but they can be indexed by values and
 
58
 not just types. It also has parameterised modules, mixfix operators, Unicode
 
59
 characters, and an interactive Emacs interface (the type checker can assist in
 
60
 the development of your code).
 
61
 .
 
62
 Agda is also a proof assistant: It is an interactive system for writing and
 
63
 checking proofs. Agda is based on intuitionistic type theory, a foundational
 
64
 system for constructive mathematics developed by the Swedish logician Per
 
65
 Martin-Löf. It has many similarities with other proof assistants based on
 
66
 dependent types, such as Coq, Epigram and NuPRL.
 
67
 .
 
68
 The Agda standard library contains modules for many common data structures and
 
69
 proof patterns. Modules provided include:
 
70
  - Algebra: Specifying and reasoning about abstract algebraic structures
 
71
  - Category: Using idioms from category theory to structure functional programs
 
72
  - Coinduction: Support for programming coindutively
 
73
  - Data: Data types and properties about data types
 
74
  - Foreign: Relating to the foreign function interface
 
75
  - Induction: A general framework for induction
 
76
  - IO: Input/output related functions
 
77
  - Level: Universe levels
 
78
  - Relations: Properties of and proofs about relations
 
79
  - Size: Sizes used by the sized types mechanism
 
80
 .
 
81
 This package contains the hyperlinked library documentation.