← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to README.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly

Show diffs side-by-side

added added

removed removed

Lines of Context:
README.agda
1
1
module README where
2
2
 
3
3
------------------------------------------------------------------------
 
4
-- The Agda standard library
4
5
--
5
6
-- Author: Nils Anders Danielsson, with contributions from
 
7
-- Jean-Philippe Bernardy, Peter Berry, Samuel Bronson, Daniel Brown,
 
8
-- Liang-Ting Chen, Dominique Devriese, Dan Doel, Simon Foster, Patrik
 
9
-- Jansson, Darin Morrison, Shin-Cheng Mu, Ulf Norell, Nicolas
6
10
-- Pouillard and Andrés Sicard-Ramírez
7
11
------------------------------------------------------------------------
8
12
 
 
13
-- Note that the development version of the library often requires the
 
14
-- latest development version of Agda.
9
15
 
 
16
-- Note also that no guarantees are currently made about forwards or
10
17
-- backwards compatibility, the library is still at an experimental
11
18
-- stage.
12
19
 
47
49
-- • Coinduction
48
50
--     Support for coinduction.
49
51
-- • Data
 
52
--     Data types and properties about data types.
 
53
-- • Function
 
54
--     Combinators and properties related to functions.
50
55
-- • Foreign
51
56
--     Related to the foreign function interface.
52
57
-- • Induction
59
61
--     Input/output-related functions.
60
62
-- • Level
61
63
--     Universe levels.
 
64
-- • Reflection
 
65
--     Support for reflection.
62
66
-- • Relation
63
67
--     Properties of and proofs about relations (mostly homogeneous
64
68
--     binary relations).
65
69
-- • Size
66
70
--     Sizes used by the sized types mechanism.
 
71
-- • Universe
 
72
--     A definition of universes.
67
73
 
68
74
------------------------------------------------------------------------
69
75
-- A selection of useful library modules
180
186
--       -- Reflexivity is expressed in terms of an underlying equality:
181
187
--       reflexive     : _≈_ ⇒ _∼_
182
188
--       trans         : Transitive _∼_
183
189
--
184
190
--     module Eq = IsEquivalence isEquivalence
185
191
--
 
192
--     ...
186
193
--
187
194
-- The Eq module in IsPreorder is not opened publicly, because it
188
195
-- contains some fields which clash with fields or other definitions