Index of /~nad/listings/lib-0.5

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Universe.html 20-Feb-2011 19:03 4.2K 
[TXT]Size.html 20-Feb-2011 19:03 3.4K 
[TXT]Relation.Unary.html 20-Feb-2011 19:04 66K 
[TXT]Relation.Nullary.html 20-Feb-2011 19:03 3.8K 
[TXT]Relation.Nullary.Uni..>20-Feb-2011 19:03 104K 
[TXT]Relation.Nullary.Sum..>20-Feb-2011 19:04 17K 
[TXT]Relation.Nullary.Pro..>20-Feb-2011 19:03 9.4K 
[TXT]Relation.Nullary.Neg..>20-Feb-2011 19:03 123K 
[TXT]Relation.Nullary.Dec..>20-Feb-2011 19:04 43K 
[TXT]Relation.Nullary.Cor..>20-Feb-2011 19:04 7.9K 
[TXT]Relation.Binary.html 20-Feb-2011 19:03 140K 
[TXT]Relation.Binary.Vec...>20-Feb-2011 19:04 148K 
[TXT]Relation.Binary.Sum...>20-Feb-2011 19:04 382K 
[TXT]Relation.Binary.Stri..>20-Feb-2011 19:03 69K 
[TXT]Relation.Binary.Stri..>20-Feb-2011 19:03 6.3K 
[TXT]Relation.Binary.Simp..>20-Feb-2011 19:04 14K 
[TXT]Relation.Binary.Sigm..>20-Feb-2011 19:04 237K 
[TXT]Relation.Binary.Refl..>20-Feb-2011 19:03 62K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:03 8.2K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:03 11K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:04 10K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:03 10K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:04 9.4K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:03 9.9K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:04 83K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:03 6.5K 
[TXT]Relation.Binary.Prop..>20-Feb-2011 19:03 18K 
[TXT]Relation.Binary.Prod..>20-Feb-2011 19:04 228K 
[TXT]Relation.Binary.Prod..>20-Feb-2011 19:03 254K 
[TXT]Relation.Binary.Prod..>20-Feb-2011 19:04 126K 
[TXT]Relation.Binary.Preo..>20-Feb-2011 19:03 21K 
[TXT]Relation.Binary.Part..>20-Feb-2011 19:03 5.3K 
[TXT]Relation.Binary.Orde..>20-Feb-2011 19:03 31K 
[TXT]Relation.Binary.On.html20-Feb-2011 19:03 107K 
[TXT]Relation.Binary.NonS..>20-Feb-2011 19:03 67K 
[TXT]Relation.Binary.List..>20-Feb-2011 19:03 243K 
[TXT]Relation.Binary.List..>20-Feb-2011 19:04 120K 
[TXT]Relation.Binary.List..>20-Feb-2011 19:04 108K 
[TXT]Relation.Binary.Indu..>20-Feb-2011 19:03 21K 
[TXT]Relation.Binary.Inde..>20-Feb-2011 19:04 17K 
[TXT]Relation.Binary.Inde..>20-Feb-2011 19:03 42K 
[TXT]Relation.Binary.Hete..>20-Feb-2011 19:04 153K 
[TXT]Relation.Binary.Flip..>20-Feb-2011 19:04 154K 
[TXT]Relation.Binary.EqRe..>20-Feb-2011 19:04 7.2K 
[TXT]Relation.Binary.Core..>20-Feb-2011 19:04 132K 
[TXT]Relation.Binary.Cons..>20-Feb-2011 19:03 89K 
[TXT]Relation.Binary.Cons..>20-Feb-2011 19:03 11K 
[TXT]Reflection.html 20-Feb-2011 19:04 174K 
[TXT]README.html 20-Feb-2011 19:04 35K 
[TXT]README.Nat.html 20-Feb-2011 19:04 20K 
[TXT]Level.html 20-Feb-2011 19:03 10K 
[TXT]Induction.html 20-Feb-2011 19:04 28K 
[TXT]Induction.WellFounde..>20-Feb-2011 19:04 91K 
[TXT]Induction.Nat.html 20-Feb-2011 19:03 41K 
[TXT]Induction.Lexicograp..>20-Feb-2011 19:04 51K 
[TXT]IO.html 20-Feb-2011 19:04 54K 
[TXT]IO.Primitive.html 20-Feb-2011 19:04 16K 
[TXT]Function.html 20-Feb-2011 19:04 53K 
[TXT]Function.Surjection...>20-Feb-2011 19:04 41K 
[TXT]Function.LeftInverse..>20-Feb-2011 19:04 53K 
[TXT]Function.Inverse.html 20-Feb-2011 19:03 157K 
[TXT]Function.Inverse.Typ..>20-Feb-2011 19:03 235K 
[TXT]Function.Injection.html20-Feb-2011 19:04 27K 
[TXT]Function.Equivalence..>20-Feb-2011 19:04 67K 
[TXT]Function.Equality.html 20-Feb-2011 19:04 62K 
[TXT]Function.Bijection.html20-Feb-2011 19:04 41K 
[TXT]Foreign.Haskell.html 20-Feb-2011 19:03 17K 
[TXT]Everything.html 20-Feb-2011 19:03 94K 
[TXT]Data.W.html 20-Feb-2011 19:03 18K 
[TXT]Data.Vec.html 20-Feb-2011 19:03 191K 
[TXT]Data.Vec.Properties...>20-Feb-2011 19:03 244K 
[TXT]Data.Vec.N-ary.html 20-Feb-2011 19:04 163K 
[TXT]Data.Vec.Equality.html 20-Feb-2011 19:04 78K 
[TXT]Data.Unit.html 20-Feb-2011 19:03 22K 
[TXT]Data.Sum.html 20-Feb-2011 19:03 36K 
[TXT]Data.String.html 20-Feb-2011 19:03 29K 
[TXT]Data.Stream.html 20-Feb-2011 19:03 93K 
[TXT]Data.Star.html 20-Feb-2011 19:03 99K 
[TXT]Data.Star.Vec.html 20-Feb-2011 19:04 29K 
[TXT]Data.Star.Properties..>20-Feb-2011 19:04 100K 
[TXT]Data.Star.Pointer.html 20-Feb-2011 19:03 73K 
[TXT]Data.Star.Nat.html 20-Feb-2011 19:04 19K 
[TXT]Data.Star.List.html 20-Feb-2011 19:04 9.3K 
[TXT]Data.Star.Fin.html 20-Feb-2011 19:04 8.8K 
[TXT]Data.Star.Environmen..>20-Feb-2011 19:03 19K 
[TXT]Data.Star.Decoration..>20-Feb-2011 19:04 74K 
[TXT]Data.Star.BoundedVec..>20-Feb-2011 19:04 28K 
[TXT]Data.Sign.html 20-Feb-2011 19:03 11K 
[TXT]Data.Sign.Properties..>20-Feb-2011 19:04 11K 
[TXT]Data.ReflexiveClosur..>20-Feb-2011 19:03 26K 
[TXT]Data.Rational.html 20-Feb-2011 19:04 63K 
[TXT]Data.Product.html 20-Feb-2011 19:03 91K 
[TXT]Data.Product.N-ary.html20-Feb-2011 19:03 41K 
[TXT]Data.Plus.html 20-Feb-2011 19:04 51K 
[TXT]Data.Nat.html 20-Feb-2011 19:03 124K 
[TXT]Data.Nat.Show.html 20-Feb-2011 19:03 11K 
[TXT]Data.Nat.Properties...>20-Feb-2011 19:04 399K 
[TXT]Data.Nat.LCM.html 20-Feb-2011 19:03 90K 
[TXT]Data.Nat.InfinitelyO..>20-Feb-2011 19:03 57K 
[TXT]Data.Nat.GCD.html 20-Feb-2011 19:04 127K 
[TXT]Data.Nat.GCD.Lemmas...>20-Feb-2011 19:03 225K 
[TXT]Data.Nat.Divisibilit..>20-Feb-2011 19:03 133K 
[TXT]Data.Nat.DivMod.html 20-Feb-2011 19:03 79K 
[TXT]Data.Nat.Coprimality..>20-Feb-2011 19:04 96K 
[TXT]Data.Maybe.html 20-Feb-2011 19:03 106K 
[TXT]Data.Maybe.Core.html 20-Feb-2011 19:03 4.6K 
[TXT]Data.List.html 20-Feb-2011 19:04 214K 
[TXT]Data.List.Reverse.html 20-Feb-2011 19:03 28K 
[TXT]Data.List.Properties..>20-Feb-2011 19:03 487K 
[TXT]Data.List.NonEmpty.html20-Feb-2011 19:04 138K 
[TXT]Data.List.NonEmpty.P..>20-Feb-2011 19:03 48K 
[TXT]Data.List.Countdown...>20-Feb-2011 19:03 197K 
[TXT]Data.List.Any.html 20-Feb-2011 19:04 134K 
[TXT]Data.List.Any.Proper..>20-Feb-2011 19:03 625K 
[TXT]Data.List.Any.Member..>20-Feb-2011 19:03 245K 
[TXT]Data.List.Any.BagAnd..>20-Feb-2011 19:04 289K 
[TXT]Data.List.All.html 20-Feb-2011 19:04 49K 
[TXT]Data.List.All.Proper..>20-Feb-2011 19:03 54K 
[TXT]Data.Integer.html 20-Feb-2011 19:04 156K 
[TXT]Data.Integer.Propert..>20-Feb-2011 19:04 80K 
[TXT]Data.Integer.Divisib..>20-Feb-2011 19:04 13K 
[TXT]Data.Graph.Acyclic.html20-Feb-2011 19:04 194K 
[TXT]Data.Fin.html 20-Feb-2011 19:04 109K 
[TXT]Data.Fin.Substitutio..>20-Feb-2011 19:03 83K 
[TXT]Data.Fin.Substitutio..>20-Feb-2011 19:03 23K 
[TXT]Data.Fin.Substitutio..>20-Feb-2011 19:04 499K 
[TXT]Data.Fin.Substitutio..>20-Feb-2011 19:03 73K 
[TXT]Data.Fin.Subset.html 20-Feb-2011 19:03 42K 
[TXT]Data.Fin.Subset.Prop..>20-Feb-2011 19:04 118K 
[TXT]Data.Fin.Props.html 20-Feb-2011 19:04 134K 
[TXT]Data.Fin.Dec.html 20-Feb-2011 19:04 139K 
[TXT]Data.Empty.html 20-Feb-2011 19:03 3.8K 
[TXT]Data.Digit.html 20-Feb-2011 19:04 61K 
[TXT]Data.DifferenceVec.html20-Feb-2011 19:03 36K 
[TXT]Data.DifferenceNat.html20-Feb-2011 19:03 12K 
[TXT]Data.DifferenceList...>20-Feb-2011 19:04 33K 
[TXT]Data.Covec.html 20-Feb-2011 19:04 110K 
[TXT]Data.Context.html 20-Feb-2011 19:04 76K 
[TXT]Data.Container.html 20-Feb-2011 19:04 192K 
[TXT]Data.Container.Combi..>20-Feb-2011 19:04 159K 
[TXT]Data.Container.Any.html20-Feb-2011 19:03 256K 
[TXT]Data.Conat.html 20-Feb-2011 19:04 25K 
[TXT]Data.Colist.html 20-Feb-2011 19:04 178K 
[TXT]Data.Cofin.html 20-Feb-2011 19:04 19K 
[TXT]Data.Char.html 20-Feb-2011 19:03 15K 
[TXT]Data.BoundedVec.html 20-Feb-2011 19:03 38K 
[TXT]Data.BoundedVec.Inef..>20-Feb-2011 19:04 20K 
[TXT]Data.Bool.html 20-Feb-2011 19:03 26K 
[TXT]Data.Bool.Show.html 20-Feb-2011 19:03 3.4K 
[TXT]Data.Bool.Properties..>20-Feb-2011 19:03 142K 
[TXT]Data.Bin.html 20-Feb-2011 19:03 173K 
[TXT]Data.AVL.html 20-Feb-2011 19:03 215K 
[TXT]Data.AVL.Sets.html 20-Feb-2011 19:03 26K 
[TXT]Data.AVL.IndexedMap...>20-Feb-2011 19:03 46K 
[TXT]Coinduction.html 20-Feb-2011 19:04 13K 
[TXT]Category.Monad.html 20-Feb-2011 19:03 17K 
[TXT]Category.Monad.State..>20-Feb-2011 19:04 84K 
[TXT]Category.Monad.Parti..>20-Feb-2011 19:04 695K 
[TXT]Category.Monad.Index..>20-Feb-2011 19:04 36K 
[TXT]Category.Monad.Ident..>20-Feb-2011 19:03 6.6K 
[TXT]Category.Monad.Conti..>20-Feb-2011 19:03 44K 
[TXT]Category.Functor.html 20-Feb-2011 19:03 8.2K 
[TXT]Category.Applicative..>20-Feb-2011 19:04 7.7K 
[TXT]Category.Applicative..>20-Feb-2011 19:03 62K 
[TXT]Algebra.html 20-Feb-2011 19:04 155K 
[TXT]Algebra.Structures.html20-Feb-2011 19:04 210K 
[TXT]Algebra.RingSolver.html20-Feb-2011 19:04 195K 
[TXT]Algebra.RingSolver.S..>20-Feb-2011 19:03 5.1K 
[TXT]Algebra.RingSolver.L..>20-Feb-2011 19:04 143K 
[TXT]Algebra.RingSolver.A..>20-Feb-2011 19:04 61K 
[TXT]Algebra.Props.Ring.html20-Feb-2011 19:03 42K 
[TXT]Algebra.Props.Lattic..>20-Feb-2011 19:03 66K 
[TXT]Algebra.Props.Group...>20-Feb-2011 19:03 59K 
[TXT]Algebra.Props.Distri..>20-Feb-2011 19:03 59K 
[TXT]Algebra.Props.Boolea..>20-Feb-2011 19:03 504K 
[TXT]Algebra.Props.Boolea..>20-Feb-2011 19:03 159K 
[TXT]Algebra.Props.Abelia..>20-Feb-2011 19:03 34K 
[TXT]Algebra.Operations.html20-Feb-2011 19:04 32K 
[TXT]Algebra.Morphism.html 20-Feb-2011 19:04 45K 
[TXT]Algebra.FunctionProp..>20-Feb-2011 19:04 60K 
[TXT]Algebra.FunctionProp..>20-Feb-2011 19:03 6.7K 
[TXT]Agda.css 20-Feb-2011 19:04 1.1K 

README
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