← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

Viewing changes to Everything.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:
Everything.agda
26
26
-- Some derivable properties
27
27
import Algebra.Props.BooleanAlgebra
28
28
 
 
29
-- Boolean algebra expressions
 
30
import Algebra.Props.BooleanAlgebra.Expression
 
31
 
29
32
-- Some derivable properties
30
33
import Algebra.Props.DistributiveLattice
31
34
 
82
85
-- The state monad
83
86
import Category.Monad.State
84
87
 
 
88
-- Basic types related to coinduction
85
89
import Coinduction
86
90
 
87
91
-- AVL trees
124
127
-- Coinductive "natural" numbers
125
128
import Data.Conat
126
129
 
 
130
-- Containers, based on the work of Abbott and others
 
131
import Data.Container
 
132
 
 
133
-- Properties related to ◇
 
134
import Data.Container.Any
 
135
 
 
136
-- Container combinators
 
137
import Data.Container.Combinator
 
138
 
 
139
-- Contexts, variables, substitutions, etc.
 
140
import Data.Context
 
141
 
127
142
-- Coinductive vectors
128
143
import Data.Covec
129
144
 
172
187
-- Application of substitutions to lists, along with various lemmas
173
188
import Data.Fin.Substitution.List
174
189
 
175
 
import Data.Function
176
 
 
177
 
import Data.Function.Equality
178
 
 
179
 
import Data.Function.Injection
180
 
 
181
 
import Data.Function.LeftInverse
182
 
 
183
190
-- Directed acyclic multigraphs
184
191
import Data.Graph.Acyclic
185
192
 
208
211
-- Lists where at least one element satisfies a given property
209
212
import Data.List.Any
210
213
 
 
214
-- Properties related to bag and set equality
 
215
import Data.List.Any.BagAndSetEquality
 
216
 
 
217
-- Properties related to list membership
 
218
import Data.List.Any.Membership
 
219
 
 
220
-- Properties related to Any
211
221
import Data.List.Any.Properties
212
222
 
213
223
-- A data structure which keeps track of an upper bound on the number
227
236
-- Reverse view
228
237
import Data.List.Reverse
229
238
 
230
 
import Data.Map
231
 
 
232
239
-- The Maybe type
233
240
import Data.Maybe
234
241
 
264
269
-- Showing natural numbers
265
270
import Data.Nat.Show
266
271
 
 
272
-- Transitive closures
 
273
import Data.Plus
 
274
 
267
275
-- Products
268
276
import Data.Product
269
277
 
270
 
import Data.Product.Record
 
278
-- N-ary products
 
279
import Data.Product.N-ary
271
280
 
272
281
-- Rational numbers
273
282
import Data.Rational
274
283
 
275
 
import Data.Sets
 
284
-- Reflexive closures
 
285
import Data.ReflexiveClosure
276
286
 
277
287
-- Signs
278
288
import Data.Sign
336
344
-- Some Vec-related properties
337
345
import Data.Vec.Properties
338
346
 
 
347
-- W-types
 
348
import Data.W
 
349
 
339
350
-- Types used (only) when calling out to Haskell via the FFI
340
351
import Foreign.Haskell
341
352
 
 
353
-- Simple combinators working solely on and with functions
 
354
import Function
 
355
 
 
356
-- Bijections
 
357
import Function.Bijection
 
358
 
 
359
-- Function setoids and related constructions
 
360
import Function.Equality
 
361
 
 
362
-- Equivalence (coinhabitance)
 
363
import Function.Equivalence
 
364
 
 
365
-- Injections
 
366
import Function.Injection
 
367
 
 
368
-- Inverses
 
369
import Function.Inverse
 
370
 
 
371
-- Various basic type isomorphisms
 
372
import Function.Inverse.TypeIsomorphisms
 
373
 
 
374
-- Left inverses
 
375
import Function.LeftInverse
 
376
 
 
377
-- Surjections
 
378
import Function.Surjection
 
379
 
342
380
-- IO
343
381
import IO
344
382
 
360
398
-- Universe levels
361
399
import Level
362
400
 
 
401
-- Support for reflection
 
402
import Reflection
 
403
 
363
404
-- Properties of homogeneous binary relations
364
405
import Relation.Binary
365
406
 
375
416
-- Heterogeneous equality
376
417
import Relation.Binary.HeterogeneousEquality
377
418
 
 
419
-- Indexed binary relations
 
420
import Relation.Binary.Indexed
 
421
 
378
422
-- Induced preorders
379
423
import Relation.Binary.InducedPreorders
380
424
 
439
483
-- proof by reflection
440
484
import Relation.Binary.Reflection
441
485
 
 
486
-- Pointwise lifting of binary relations to sigma types
 
487
import Relation.Binary.Sigma.Pointwise
 
488
 
442
489
-- Some simple binary relations
443
490
import Relation.Binary.Simple
444
491
 
452
499
-- Sums of binary relations
453
500
import Relation.Binary.Sum
454
501
 
 
502
-- Pointwise lifting of relations to vectors
 
503
import Relation.Binary.Vec.Pointwise
 
504
 
455
505
-- Operations on nullary relations (like negation and decidability)
456
506
import Relation.Nullary
457
507
 
475
525
 
476
526
-- Sizes for Agda's sized types
477
527
import Size
 
528
 
 
529
-- Universes
 
530
import Universe