~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to README.txt

Committer: Bazaar Package Importer
Author(s): Iain Lane
Date: 2010-01-08 23:35:09 UTC
Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb

Import upstream version 0.3

files added:

.boring

AllNonAsciiChars.hs

Everything.agda

GNUmakefile

GenerateEverything.hs

Header

LICENCE

README

README.agda

README.txt

README/Nat.agda

release-notes

src/Algebra

src/Algebra.agda

src/Algebra/FunctionProperties

src/Algebra/FunctionProperties.agda

src/Algebra/FunctionProperties/Core.agda

src/Algebra/Morphism.agda

src/Algebra/Operations.agda

src/Algebra/Props

src/Algebra/Props/AbelianGroup.agda

src/Algebra/Props/BooleanAlgebra.agda

src/Algebra/Props/DistributiveLattice.agda

src/Algebra/Props/Group.agda

src/Algebra/Props/Lattice.agda

src/Algebra/Props/Ring.agda

src/Algebra/RingSolver

src/Algebra/RingSolver.agda

src/Algebra/RingSolver/AlmostCommutativeRing.agda

src/Algebra/RingSolver/Lemmas.agda

src/Algebra/RingSolver/Simple.agda

src/Algebra/Structures.agda

src/Category

src/Category/Applicative

src/Category/Applicative.agda

src/Category/Applicative/Indexed.agda

src/Category/Functor.agda

src/Category/Monad

src/Category/Monad.agda

src/Category/Monad/Continuation.agda

src/Category/Monad/Identity.agda

src/Category/Monad/Indexed.agda

src/Category/Monad/Partiality.agda

src/Category/Monad/State.agda

src/Coinduction.agda

src/Data

src/Data/AVL

src/Data/AVL.agda

src/Data/AVL/IndexedMap.agda

src/Data/AVL/Sets.agda

src/Data/Bin.agda

src/Data/Bool

src/Data/Bool.agda

src/Data/Bool/Properties.agda

src/Data/Bool/Show.agda

src/Data/BoundedVec

src/Data/BoundedVec.agda

src/Data/BoundedVec/Inefficient.agda

src/Data/Char.agda

src/Data/Cofin.agda

src/Data/Colist.agda

src/Data/Conat.agda

src/Data/Covec.agda

src/Data/DifferenceList.agda

src/Data/DifferenceNat.agda

src/Data/DifferenceVec.agda

src/Data/Digit.agda

src/Data/Empty.agda

src/Data/Fin

src/Data/Fin.agda

src/Data/Fin/Dec.agda

src/Data/Fin/Props.agda

src/Data/Fin/Subset

src/Data/Fin/Subset.agda

src/Data/Fin/Subset/Props.agda

src/Data/Fin/Substitution

src/Data/Fin/Substitution.agda

src/Data/Fin/Substitution/Example.agda

src/Data/Fin/Substitution/Lemmas.agda

src/Data/Fin/Substitution/List.agda

src/Data/Function

src/Data/Function.agda

src/Data/Function/Equality.agda

src/Data/Function/Injection.agda

src/Data/Function/LeftInverse.agda

src/Data/Graph

src/Data/Graph/Acyclic.agda

src/Data/Integer

src/Data/Integer.agda

src/Data/Integer/Divisibility.agda

src/Data/Integer/Properties.agda

src/Data/List

src/Data/List.agda

src/Data/List/All

src/Data/List/All.agda

src/Data/List/All/Properties.agda

src/Data/List/Any

src/Data/List/Any.agda

src/Data/List/Any/Properties.agda

src/Data/List/Countdown.agda

src/Data/List/NonEmpty

src/Data/List/NonEmpty.agda

src/Data/List/NonEmpty/Properties.agda

src/Data/List/Properties.agda

src/Data/List/Reverse.agda

src/Data/Map.agda

src/Data/Maybe

src/Data/Maybe.agda

src/Data/Maybe/Core.agda

src/Data/Nat

src/Data/Nat.agda

src/Data/Nat/Coprimality.agda

src/Data/Nat/DivMod.agda

src/Data/Nat/Divisibility.agda

src/Data/Nat/GCD

src/Data/Nat/GCD.agda

src/Data/Nat/GCD/Lemmas.agda

src/Data/Nat/InfinitelyOften.agda

src/Data/Nat/LCM.agda

src/Data/Nat/Properties.agda

src/Data/Nat/Show.agda

src/Data/Product

src/Data/Product.agda

src/Data/Product/Record.agda

src/Data/Rational.agda

src/Data/Sets.agda

src/Data/Sign

src/Data/Sign.agda

src/Data/Sign/Properties.agda

src/Data/Star

src/Data/Star.agda

src/Data/Star/BoundedVec.agda

src/Data/Star/Decoration.agda

src/Data/Star/Environment.agda

src/Data/Star/Fin.agda

src/Data/Star/List.agda

src/Data/Star/Nat.agda

src/Data/Star/Pointer.agda

src/Data/Star/Properties.agda

src/Data/Star/Vec.agda

src/Data/Stream.agda

src/Data/String.agda

src/Data/Sum.agda

src/Data/Unit.agda

src/Data/Vec

src/Data/Vec.agda

src/Data/Vec/Equality.agda

src/Data/Vec/N-ary.agda

src/Data/Vec/Properties.agda

src/Foreign

src/Foreign/Haskell.agda

src/IO

src/IO.agda

src/IO/Primitive.agda

src/Induction

src/Induction.agda

src/Induction/Lexicographic.agda

src/Induction/Nat.agda

src/Induction/WellFounded.agda

src/Level.agda

src/Relation

src/Relation/Binary

src/Relation/Binary.agda

src/Relation/Binary/Consequences

src/Relation/Binary/Consequences.agda

src/Relation/Binary/Consequences/Core.agda

src/Relation/Binary/Core.agda

src/Relation/Binary/EqReasoning.agda

src/Relation/Binary/Flip.agda

src/Relation/Binary/HeterogeneousEquality.agda

src/Relation/Binary/InducedPreorders.agda

src/Relation/Binary/List

src/Relation/Binary/List/NonStrictLex.agda

src/Relation/Binary/List/Pointwise.agda

src/Relation/Binary/List/StrictLex.agda

src/Relation/Binary/NonStrictToStrict.agda

src/Relation/Binary/On.agda

src/Relation/Binary/OrderMorphism.agda

src/Relation/Binary/PartialOrderReasoning.agda

src/Relation/Binary/PreorderReasoning.agda

src/Relation/Binary/Product

src/Relation/Binary/Product/NonStrictLex.agda

src/Relation/Binary/Product/Pointwise.agda

src/Relation/Binary/Product/StrictLex.agda

src/Relation/Binary/PropositionalEquality

src/Relation/Binary/PropositionalEquality.agda

src/Relation/Binary/PropositionalEquality/Core.agda

src/Relation/Binary/PropositionalEquality/TrustMe.agda

src/Relation/Binary/Props

src/Relation/Binary/Props/DecTotalOrder.agda

src/Relation/Binary/Props/Poset.agda

src/Relation/Binary/Props/Preorder.agda

src/Relation/Binary/Props/StrictPartialOrder.agda

src/Relation/Binary/Props/StrictTotalOrder.agda

src/Relation/Binary/Props/TotalOrder.agda

src/Relation/Binary/Reflection.agda

src/Relation/Binary/Simple.agda

src/Relation/Binary/StrictPartialOrderReasoning.agda

src/Relation/Binary/StrictToNonStrict.agda

src/Relation/Binary/Sum.agda

src/Relation/Nullary

src/Relation/Nullary.agda

src/Relation/Nullary/Core.agda

src/Relation/Nullary/Decidable.agda

src/Relation/Nullary/Negation.agda

src/Relation/Nullary/Product.agda

src/Relation/Nullary/Sum.agda

src/Relation/Nullary/Universe.agda

src/Relation/Unary.agda

src/Size.agda

Show diffs side-by-side

added added

removed removed

README.txt

------------------------------------------------------------------------

The Agda standard library

------------------------------------------------------------------------

For information about the library, see README.agda.

The README module imports the Everything module. This module is

generated automatically; if you have downloaded the library from its

darcs repository and want to type check README you can construct

Everything by running "runhaskell GenerateEverything.hs". Note that

the GenerateEverything program depends on the filepath and FileManip

packages from Hackage.

Note that all library sources are located under src. The modules

README and Everything are not really part of the library, so these

modules are located in the top-level directory instead.

Older »