Name | Last modified | Size | Description | |
---|---|---|---|---|
Parent Directory | - | |||
Agda.css | 2011-02-20 19:04 | 1.1K | ||
Algebra.FunctionProp..> | 2011-02-20 19:03 | 6.7K | ||
Algebra.FunctionProp..> | 2011-02-20 19:04 | 60K | ||
Algebra.Morphism.html | 2011-02-20 19:04 | 45K | ||
Algebra.Operations.html | 2011-02-20 19:04 | 32K | ||
Algebra.Props.Abelia..> | 2011-02-20 19:03 | 34K | ||
Algebra.Props.Boolea..> | 2011-02-20 19:03 | 159K | ||
Algebra.Props.Boolea..> | 2011-02-20 19:03 | 504K | ||
Algebra.Props.Distri..> | 2011-02-20 19:03 | 59K | ||
Algebra.Props.Group...> | 2011-02-20 19:03 | 59K | ||
Algebra.Props.Lattic..> | 2011-02-20 19:03 | 66K | ||
Algebra.Props.Ring.html | 2011-02-20 19:03 | 42K | ||
Algebra.RingSolver.A..> | 2011-02-20 19:04 | 61K | ||
Algebra.RingSolver.L..> | 2011-02-20 19:04 | 143K | ||
Algebra.RingSolver.S..> | 2011-02-20 19:03 | 5.1K | ||
Algebra.RingSolver.html | 2011-02-20 19:04 | 195K | ||
Algebra.Structures.html | 2011-02-20 19:04 | 210K | ||
Algebra.html | 2011-02-20 19:04 | 155K | ||
Category.Applicative..> | 2011-02-20 19:03 | 62K | ||
Category.Applicative..> | 2011-02-20 19:04 | 7.7K | ||
Category.Functor.html | 2011-02-20 19:03 | 8.2K | ||
Category.Monad.Conti..> | 2011-02-20 19:03 | 44K | ||
Category.Monad.Ident..> | 2011-02-20 19:03 | 6.6K | ||
Category.Monad.Index..> | 2011-02-20 19:04 | 36K | ||
Category.Monad.Parti..> | 2011-02-20 19:04 | 695K | ||
Category.Monad.State..> | 2011-02-20 19:04 | 84K | ||
Category.Monad.html | 2011-02-20 19:03 | 17K | ||
Coinduction.html | 2011-02-20 19:04 | 13K | ||
Data.AVL.IndexedMap...> | 2011-02-20 19:03 | 46K | ||
Data.AVL.Sets.html | 2011-02-20 19:03 | 26K | ||
Data.AVL.html | 2011-02-20 19:03 | 215K | ||
Data.Bin.html | 2011-02-20 19:03 | 173K | ||
Data.Bool.Properties..> | 2011-02-20 19:03 | 142K | ||
Data.Bool.Show.html | 2011-02-20 19:03 | 3.4K | ||
Data.Bool.html | 2011-02-20 19:03 | 26K | ||
Data.BoundedVec.Inef..> | 2011-02-20 19:04 | 20K | ||
Data.BoundedVec.html | 2011-02-20 19:03 | 38K | ||
Data.Char.html | 2011-02-20 19:03 | 15K | ||
Data.Cofin.html | 2011-02-20 19:04 | 19K | ||
Data.Colist.html | 2011-02-20 19:04 | 178K | ||
Data.Conat.html | 2011-02-20 19:04 | 25K | ||
Data.Container.Any.html | 2011-02-20 19:03 | 256K | ||
Data.Container.Combi..> | 2011-02-20 19:04 | 159K | ||
Data.Container.html | 2011-02-20 19:04 | 192K | ||
Data.Context.html | 2011-02-20 19:04 | 76K | ||
Data.Covec.html | 2011-02-20 19:04 | 110K | ||
Data.DifferenceList...> | 2011-02-20 19:04 | 33K | ||
Data.DifferenceNat.html | 2011-02-20 19:03 | 12K | ||
Data.DifferenceVec.html | 2011-02-20 19:03 | 36K | ||
Data.Digit.html | 2011-02-20 19:04 | 61K | ||
Data.Empty.html | 2011-02-20 19:03 | 3.8K | ||
Data.Fin.Dec.html | 2011-02-20 19:04 | 139K | ||
Data.Fin.Props.html | 2011-02-20 19:04 | 134K | ||
Data.Fin.Subset.Prop..> | 2011-02-20 19:04 | 118K | ||
Data.Fin.Subset.html | 2011-02-20 19:03 | 42K | ||
Data.Fin.Substitutio..> | 2011-02-20 19:03 | 73K | ||
Data.Fin.Substitutio..> | 2011-02-20 19:04 | 499K | ||
Data.Fin.Substitutio..> | 2011-02-20 19:03 | 23K | ||
Data.Fin.Substitutio..> | 2011-02-20 19:03 | 83K | ||
Data.Fin.html | 2011-02-20 19:04 | 109K | ||
Data.Graph.Acyclic.html | 2011-02-20 19:04 | 194K | ||
Data.Integer.Divisib..> | 2011-02-20 19:04 | 13K | ||
Data.Integer.Propert..> | 2011-02-20 19:04 | 80K | ||
Data.Integer.html | 2011-02-20 19:04 | 156K | ||
Data.List.All.Proper..> | 2011-02-20 19:03 | 54K | ||
Data.List.All.html | 2011-02-20 19:04 | 49K | ||
Data.List.Any.BagAnd..> | 2011-02-20 19:04 | 289K | ||
Data.List.Any.Member..> | 2011-02-20 19:03 | 245K | ||
Data.List.Any.Proper..> | 2011-02-20 19:03 | 625K | ||
Data.List.Any.html | 2011-02-20 19:04 | 134K | ||
Data.List.Countdown...> | 2011-02-20 19:03 | 197K | ||
Data.List.NonEmpty.P..> | 2011-02-20 19:03 | 48K | ||
Data.List.NonEmpty.html | 2011-02-20 19:04 | 138K | ||
Data.List.Properties..> | 2011-02-20 19:03 | 487K | ||
Data.List.Reverse.html | 2011-02-20 19:03 | 28K | ||
Data.List.html | 2011-02-20 19:04 | 214K | ||
Data.Maybe.Core.html | 2011-02-20 19:03 | 4.6K | ||
Data.Maybe.html | 2011-02-20 19:03 | 106K | ||
Data.Nat.Coprimality..> | 2011-02-20 19:04 | 96K | ||
Data.Nat.DivMod.html | 2011-02-20 19:03 | 79K | ||
Data.Nat.Divisibilit..> | 2011-02-20 19:03 | 133K | ||
Data.Nat.GCD.Lemmas...> | 2011-02-20 19:03 | 225K | ||
Data.Nat.GCD.html | 2011-02-20 19:04 | 127K | ||
Data.Nat.InfinitelyO..> | 2011-02-20 19:03 | 57K | ||
Data.Nat.LCM.html | 2011-02-20 19:03 | 90K | ||
Data.Nat.Properties...> | 2011-02-20 19:04 | 399K | ||
Data.Nat.Show.html | 2011-02-20 19:03 | 11K | ||
Data.Nat.html | 2011-02-20 19:03 | 124K | ||
Data.Plus.html | 2011-02-20 19:04 | 51K | ||
Data.Product.N-ary.html | 2011-02-20 19:03 | 41K | ||
Data.Product.html | 2011-02-20 19:03 | 91K | ||
Data.Rational.html | 2011-02-20 19:04 | 63K | ||
Data.ReflexiveClosur..> | 2011-02-20 19:03 | 26K | ||
Data.Sign.Properties..> | 2011-02-20 19:04 | 11K | ||
Data.Sign.html | 2011-02-20 19:03 | 11K | ||
Data.Star.BoundedVec..> | 2011-02-20 19:04 | 28K | ||
Data.Star.Decoration..> | 2011-02-20 19:04 | 74K | ||
Data.Star.Environmen..> | 2011-02-20 19:03 | 19K | ||
Data.Star.Fin.html | 2011-02-20 19:04 | 8.8K | ||
Data.Star.List.html | 2011-02-20 19:04 | 9.3K | ||
Data.Star.Nat.html | 2011-02-20 19:04 | 19K | ||
Data.Star.Pointer.html | 2011-02-20 19:03 | 73K | ||
Data.Star.Properties..> | 2011-02-20 19:04 | 100K | ||
Data.Star.Vec.html | 2011-02-20 19:04 | 29K | ||
Data.Star.html | 2011-02-20 19:03 | 99K | ||
Data.Stream.html | 2011-02-20 19:03 | 93K | ||
Data.String.html | 2011-02-20 19:03 | 29K | ||
Data.Sum.html | 2011-02-20 19:03 | 36K | ||
Data.Unit.html | 2011-02-20 19:03 | 22K | ||
Data.Vec.Equality.html | 2011-02-20 19:04 | 78K | ||
Data.Vec.N-ary.html | 2011-02-20 19:04 | 163K | ||
Data.Vec.Properties...> | 2011-02-20 19:03 | 244K | ||
Data.Vec.html | 2011-02-20 19:03 | 191K | ||
Data.W.html | 2011-02-20 19:03 | 18K | ||
Everything.html | 2011-02-20 19:03 | 94K | ||
Foreign.Haskell.html | 2011-02-20 19:03 | 17K | ||
Function.Bijection.html | 2011-02-20 19:04 | 41K | ||
Function.Equality.html | 2011-02-20 19:04 | 62K | ||
Function.Equivalence..> | 2011-02-20 19:04 | 67K | ||
Function.Injection.html | 2011-02-20 19:04 | 27K | ||
Function.Inverse.Typ..> | 2011-02-20 19:03 | 235K | ||
Function.Inverse.html | 2011-02-20 19:03 | 157K | ||
Function.LeftInverse..> | 2011-02-20 19:04 | 53K | ||
Function.Surjection...> | 2011-02-20 19:04 | 41K | ||
Function.html | 2011-02-20 19:04 | 53K | ||
IO.Primitive.html | 2011-02-20 19:04 | 16K | ||
IO.html | 2011-02-20 19:04 | 54K | ||
Induction.Lexicograp..> | 2011-02-20 19:04 | 51K | ||
Induction.Nat.html | 2011-02-20 19:03 | 41K | ||
Induction.WellFounde..> | 2011-02-20 19:04 | 91K | ||
Induction.html | 2011-02-20 19:04 | 28K | ||
Level.html | 2011-02-20 19:03 | 10K | ||
Reflection.html | 2011-02-20 19:04 | 174K | ||
Relation.Binary.Cons..> | 2011-02-20 19:03 | 11K | ||
Relation.Binary.Cons..> | 2011-02-20 19:03 | 89K | ||
Relation.Binary.Core..> | 2011-02-20 19:04 | 132K | ||
Relation.Binary.EqRe..> | 2011-02-20 19:04 | 7.2K | ||
Relation.Binary.Flip..> | 2011-02-20 19:04 | 154K | ||
Relation.Binary.Hete..> | 2011-02-20 19:04 | 153K | ||
Relation.Binary.Inde..> | 2011-02-20 19:03 | 42K | ||
Relation.Binary.Inde..> | 2011-02-20 19:04 | 17K | ||
Relation.Binary.Indu..> | 2011-02-20 19:03 | 21K | ||
Relation.Binary.List..> | 2011-02-20 19:04 | 108K | ||
Relation.Binary.List..> | 2011-02-20 19:04 | 120K | ||
Relation.Binary.List..> | 2011-02-20 19:03 | 243K | ||
Relation.Binary.NonS..> | 2011-02-20 19:03 | 67K | ||
Relation.Binary.On.html | 2011-02-20 19:03 | 107K | ||
Relation.Binary.Orde..> | 2011-02-20 19:03 | 31K | ||
Relation.Binary.Part..> | 2011-02-20 19:03 | 5.3K | ||
Relation.Binary.Preo..> | 2011-02-20 19:03 | 21K | ||
Relation.Binary.Prod..> | 2011-02-20 19:04 | 126K | ||
Relation.Binary.Prod..> | 2011-02-20 19:03 | 254K | ||
Relation.Binary.Prod..> | 2011-02-20 19:04 | 228K | ||
Relation.Binary.Prop..> | 2011-02-20 19:03 | 18K | ||
Relation.Binary.Prop..> | 2011-02-20 19:03 | 6.5K | ||
Relation.Binary.Prop..> | 2011-02-20 19:04 | 83K | ||
Relation.Binary.Prop..> | 2011-02-20 19:03 | 9.9K | ||
Relation.Binary.Prop..> | 2011-02-20 19:04 | 9.4K | ||
Relation.Binary.Prop..> | 2011-02-20 19:03 | 10K | ||
Relation.Binary.Prop..> | 2011-02-20 19:04 | 10K | ||
Relation.Binary.Prop..> | 2011-02-20 19:03 | 11K | ||
Relation.Binary.Prop..> | 2011-02-20 19:03 | 8.2K | ||
Relation.Binary.Refl..> | 2011-02-20 19:03 | 62K | ||
Relation.Binary.Sigm..> | 2011-02-20 19:04 | 237K | ||
Relation.Binary.Simp..> | 2011-02-20 19:04 | 14K | ||
Relation.Binary.Stri..> | 2011-02-20 19:03 | 6.3K | ||
Relation.Binary.Stri..> | 2011-02-20 19:03 | 69K | ||
Relation.Binary.Sum...> | 2011-02-20 19:04 | 382K | ||
Relation.Binary.Vec...> | 2011-02-20 19:04 | 148K | ||
Relation.Binary.html | 2011-02-20 19:03 | 140K | ||
Relation.Nullary.Cor..> | 2011-02-20 19:04 | 7.9K | ||
Relation.Nullary.Dec..> | 2011-02-20 19:04 | 43K | ||
Relation.Nullary.Neg..> | 2011-02-20 19:03 | 123K | ||
Relation.Nullary.Pro..> | 2011-02-20 19:03 | 9.4K | ||
Relation.Nullary.Sum..> | 2011-02-20 19:04 | 17K | ||
Relation.Nullary.Uni..> | 2011-02-20 19:03 | 104K | ||
Relation.Nullary.html | 2011-02-20 19:03 | 3.8K | ||
Relation.Unary.html | 2011-02-20 19:04 | 66K | ||
Size.html | 2011-02-20 19:03 | 3.4K | ||
Universe.html | 2011-02-20 19:03 | 4.2K | ||
module README where ------------------------------------------------------------------------ -- The Agda standard library, version 0.5 -- -- Author: Nils Anders Danielsson, with contributions from -- Jean-Philippe Bernardy, Peter Berry, Samuel Bronson, Daniel Brown, -- Liang-Ting Chen, Dominique Devriese, Dan Doel, Simon Foster, Patrik -- Jansson, Darin Morrison, Shin-Cheng Mu, Ulf Norell, Nicolas -- Pouillard and Andrés Sicard-Ramírez ------------------------------------------------------------------------ -- This version of the library has been tested using Agda 2.2.10. -- Note that no guarantees are currently made about forwards or -- backwards compatibility, the library is still at an experimental -- stage. -- To make use of the library, add the path to the library’s root -- directory (src) to the Agda search path, either using the -- --include-path flag or by customising the Emacs mode variable -- agda2-include-dirs (M-x customize-group RET agda2 RET). -- Contributions to this library are welcome (but to avoid wasted work -- it is suggested that you discuss large changes before implementing -- them). Please send contributions in the form of darcs patches (run -- darcs send --output <patch file> and attach the patch file to an -- email), and include a statement saying that you agree to release -- your library patches under the library's licence. It is appreciated -- if every patch contains a single, complete change, and if the -- coding style used in the library is adhered to. ------------------------------------------------------------------------ -- Module hierarchy ------------------------------------------------------------------------ -- The top-level module names of the library are currently allocated -- as follows: -- -- • Algebra -- Abstract algebra (monoids, groups, rings etc.), along with -- properties needed to specify these structures (associativity, -- commutativity, etc.), and operations on and proofs about the -- structures. -- • Category -- Category theory-inspired idioms used to structure functional -- programs (functors and monads, for instance). -- • Coinduction -- Support for coinduction. -- • Data -- Data types and properties about data types. -- • Function -- Combinators and properties related to functions. -- • Foreign -- Related to the foreign function interface. -- • Induction -- A general framework for induction (includes lexicographic and -- well-founded induction). -- • IO -- Input/output-related functions. -- • Level -- Universe levels. -- • Reflection -- Support for reflection. -- • Relation -- Properties of and proofs about relations (mostly homogeneous -- binary relations). -- • Size -- Sizes used by the sized types mechanism. -- • Universe -- A definition of universes. ------------------------------------------------------------------------ -- A selection of useful library modules ------------------------------------------------------------------------ -- Note that module names in source code are often hyperlinked to the -- corresponding module. In the Emacs mode you can follow these -- hyperlinks by typing M-. or clicking with the middle mouse button. -- • Some data types import Data.Bool -- Booleans. import Data.Char -- Characters. import Data.Empty -- The empty type. import Data.Fin -- Finite sets. import Data.List -- Lists. import Data.Maybe -- The maybe type. import Data.Nat -- Natural numbers. import Data.Product -- Products. import Data.Stream -- Streams. import Data.String -- Strings. import Data.Sum -- Disjoint sums. import Data.Unit -- The unit type. import Data.Vec -- Fixed-length vectors. -- • Some types used to structure computations import Category.Functor -- Functors. import Category.Applicative -- Applicative functors. import Category.Monad -- Monads. -- • Equality -- Propositional equality: import Relation.Binary.PropositionalEquality -- Convenient syntax for "equational reasoning" using a preorder: import Relation.Binary.PreorderReasoning -- Solver for commutative ring or semiring equalities: import Algebra.RingSolver -- • Properties of functions, sets and relations -- Monoids, rings and similar algebraic structures: import Algebra -- Negation, decidability, and similar operations on sets: import Relation.Nullary -- Properties of homogeneous binary relations: import Relation.Binary -- • Induction -- An abstraction of various forms of recursion/induction: import Induction -- Well-founded induction: import Induction.WellFounded -- Various forms of induction for natural numbers: import Induction.Nat -- • Support for coinduction import Coinduction -- • IO import IO ------------------------------------------------------------------------ -- Record hierarchies ------------------------------------------------------------------------ -- When an abstract hierarchy of some sort (for instance semigroup → -- monoid → group) is included in the library the basic approach is to -- specify the properties of every concept in terms of a record -- containing just properties, parameterised on the underlying -- operations, sets etc.: -- -- record IsSemigroup {A} (≈ : Rel A) (∙ : Op₂ A) : Set where -- open FunctionProperties ≈ -- field -- isEquivalence : IsEquivalence ≈ -- assoc : Associative ∙ -- ∙-cong : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈ -- -- More specific concepts are then specified in terms of the simpler -- ones: -- -- record IsMonoid {A} (≈ : Rel A) (∙ : Op₂ A) (ε : A) : Set where -- open FunctionProperties ≈ -- field -- isSemigroup : IsSemigroup ≈ ∙ -- identity : Identity ε ∙ -- -- open IsSemigroup isSemigroup public -- -- Note here that open IsSemigroup isSemigroup public ensures that the -- fields of the isSemigroup record can be accessed directly; this -- technique enables the user of an IsMonoid record to use underlying -- records without having to manually open an entire record hierarchy. -- This is not always possible, though. Consider the following definition -- of preorders: -- -- record IsPreorder {A : Set} -- (_≈_ : Rel A) -- The underlying equality. -- (_∼_ : Rel A) -- The relation. -- : Set where -- field -- isEquivalence : IsEquivalence _≈_ -- -- Reflexivity is expressed in terms of an underlying equality: -- reflexive : _≈_ ⇒ _∼_ -- trans : Transitive _∼_ -- -- module Eq = IsEquivalence isEquivalence -- -- ... -- -- The Eq module in IsPreorder is not opened publicly, because it -- contains some fields which clash with fields or other definitions -- in IsPreorder. -- Records packing up properties with the corresponding operations, -- sets, etc. are sometimes also defined: -- -- record Semigroup : Set₁ where -- infixl 7 _∙_ -- infix 4 _≈_ -- field -- Carrier : Set -- _≈_ : Rel Carrier -- _∙_ : Op₂ Carrier -- isSemigroup : IsSemigroup _≈_ _∙_ -- -- open IsSemigroup isSemigroup public -- -- setoid : Setoid -- setoid = record { isEquivalence = isEquivalence } -- -- record Monoid : Set₁ where -- infixl 7 _∙_ -- infix 4 _≈_ -- field -- Carrier : Set -- _≈_ : Rel Carrier -- _∙_ : Op₂ Carrier -- ε : Carrier -- isMonoid : IsMonoid _≈_ _∙_ ε -- -- open IsMonoid isMonoid public -- -- semigroup : Semigroup -- semigroup = record { isSemigroup = isSemigroup } -- -- open Semigroup semigroup public using (setoid) -- -- Note that the Monoid record does not include a Semigroup field. -- Instead the Monoid /module/ includes a "repackaging function" -- semigroup which converts a Monoid to a Semigroup. -- The above setup may seem a bit complicated, but we think it makes the -- library quite easy to work with, while also providing enough -- flexibility. ------------------------------------------------------------------------ -- More documentation ------------------------------------------------------------------------ -- Some examples showing where the natural numbers and some related -- operations and properties are defined, and how they can be used: import README.Nat ------------------------------------------------------------------------ -- Core modules ------------------------------------------------------------------------ -- Some modules have names ending in ".Core". These modules are -- internal, and have (mostly) been created to avoid mutual recursion -- between modules. They should not be imported directly; their -- contents are reexported by other modules. ------------------------------------------------------------------------ -- All library modules ------------------------------------------------------------------------ -- For short descriptions of every library module, see Everything: import Everything