Index of /~nad/listings/lib

	Name	Last modified	Size	Description
	Parent Directory		-
	Agda.Primitive.html	2014-01-17 16:25	7.2K
	Agda.css	2014-01-17 16:25	1.2K
	Algebra.FunctionProp..>	2014-01-17 16:25	6.3K
	Algebra.FunctionProp..>	2014-01-17 16:25	60K
	Algebra.Monoid-solve..>	2014-01-17 16:25	82K
	Algebra.Morphism.html	2014-01-17 16:25	39K
	Algebra.Operations.html	2014-01-17 16:25	108K
	Algebra.Props.Abelia..>	2014-01-17 16:25	34K
	Algebra.Props.Boolea..>	2014-01-17 16:25	151K
	Algebra.Props.Boolea..>	2014-01-17 16:25	506K
	Algebra.Props.Distri..>	2014-01-17 16:25	58K
	Algebra.Props.Group...>	2014-01-17 16:25	58K
	Algebra.Props.Lattic..>	2014-01-17 16:25	65K
	Algebra.Props.Ring.html	2014-01-17 16:25	44K
	Algebra.RingSolver.A..>	2014-01-17 16:25	64K
	Algebra.RingSolver.L..>	2014-01-17 16:25	154K
	Algebra.RingSolver.N..>	2014-01-17 16:25	35K
	Algebra.RingSolver.S..>	2014-01-17 16:25	5.8K
	Algebra.RingSolver.html	2014-01-17 16:25	492K
	Algebra.Structures.html	2014-01-17 16:25	209K
	Algebra.html	2014-01-17 16:25	155K
	Category.Applicative..>	2014-01-17 16:25	60K
	Category.Applicative..>	2014-01-17 16:25	7.2K
	Category.Functor.html	2014-01-17 16:25	8.1K
	Category.Monad.Conti..>	2014-01-17 16:25	43K
	Category.Monad.Ident..>	2014-01-17 16:25	6.2K
	Category.Monad.Index..>	2014-01-17 16:25	35K
	Category.Monad.Parti..>	2014-01-17 16:25	146K
	Category.Monad.Parti..>	2014-01-17 16:25	727K
	Category.Monad.State..>	2014-01-17 16:25	82K
	Category.Monad.html	2014-01-17 16:25	17K
	Coinduction.html	2014-01-17 16:25	13K
	Data.AVL.IndexedMap...>	2014-01-17 16:25	39K
	Data.AVL.Sets.html	2014-01-17 16:25	22K
	Data.AVL.html	2014-01-17 16:25	323K
	Data.Bin.html	2014-01-17 16:25	173K
	Data.Bool.Properties..>	2014-01-17 16:25	150K
	Data.Bool.Show.html	2014-01-17 16:25	3.2K
	Data.Bool.html	2014-01-17 16:25	25K
	Data.BoundedVec.Inef..>	2014-01-17 16:25	20K
	Data.BoundedVec.html	2014-01-17 16:25	39K
	Data.Char.html	2014-01-17 16:25	22K
	Data.Cofin.html	2014-01-17 16:25	19K
	Data.Colist.Infinite..>	2014-01-17 16:25	195K
	Data.Colist.html	2014-01-17 16:25	361K
	Data.Conat.html	2014-01-17 16:25	25K
	Data.Container.Any.html	2014-01-17 16:25	245K
	Data.Container.Combi..>	2014-01-17 16:25	154K
	Data.Container.FreeM..>	2014-01-17 16:25	27K
	Data.Container.html	2014-01-17 16:25	173K
	Data.Covec.html	2014-01-17 16:25	109K
	Data.DifferenceList...>	2014-01-17 16:25	39K
	Data.DifferenceNat.html	2014-01-17 16:25	11K
	Data.DifferenceVec.html	2014-01-17 16:25	40K
	Data.Digit.html	2014-01-17 16:25	57K
	Data.Empty.html	2014-01-17 16:25	4.2K
	Data.Fin.Dec.html	2014-01-17 16:25	131K
	Data.Fin.Props.html	2014-01-17 16:25	181K
	Data.Fin.Subset.Prop..>	2014-01-17 16:25	114K
	Data.Fin.Subset.html	2014-01-17 16:25	39K
	Data.Fin.Substitutio..>	2014-01-17 16:25	71K
	Data.Fin.Substitutio..>	2014-01-17 16:25	493K
	Data.Fin.Substitutio..>	2014-01-17 16:25	22K
	Data.Fin.Substitutio..>	2014-01-17 16:25	82K
	Data.Fin.html	2014-01-17 16:25	116K
	Data.Graph.Acyclic.html	2014-01-17 16:25	191K
	Data.Integer.Additio..>	2014-01-17 16:25	79K
	Data.Integer.Divisib..>	2014-01-17 16:25	11K
	Data.Integer.Multipl..>	2014-01-17 16:25	71K
	Data.Integer.Propert..>	2014-01-17 16:25	280K
	Data.Integer.html	2014-01-17 16:25	138K
	Data.List.All.Proper..>	2014-01-17 16:25	141K
	Data.List.All.html	2014-01-17 16:25	47K
	Data.List.Any.BagAnd..>	2014-01-17 16:25	252K
	Data.List.Any.Member..>	2014-01-17 16:25	251K
	Data.List.Any.Proper..>	2014-01-17 16:25	619K
	Data.List.Any.html	2014-01-17 16:25	131K
	Data.List.Countdown...>	2014-01-17 16:25	196K
	Data.List.NonEmpty.P..>	2014-01-17 16:25	31K
	Data.List.NonEmpty.html	2014-01-17 16:25	218K
	Data.List.Properties..>	2014-01-17 16:25	522K
	Data.List.Reverse.html	2014-01-17 16:25	28K
	Data.List.html	2014-01-17 16:25	214K
	Data.M.html	2014-01-17 16:25	14K
	Data.Maybe.Core.html	2014-01-17 16:25	5.0K
	Data.Maybe.html	2014-01-17 16:25	119K
	Data.Nat.Coprimality..>	2014-01-17 16:25	115K
	Data.Nat.DivMod.html	2014-01-17 16:25	68K
	Data.Nat.Divisibilit..>	2014-01-17 16:25	128K
	Data.Nat.GCD.Lemmas...>	2014-01-17 16:25	223K
	Data.Nat.GCD.html	2014-01-17 16:25	122K
	Data.Nat.InfinitelyO..>	2014-01-17 16:25	56K
	Data.Nat.LCM.html	2014-01-17 16:25	87K
	Data.Nat.Primality.html	2014-01-17 16:25	13K
	Data.Nat.Properties...>	2014-01-17 16:25	459K
	Data.Nat.Show.html	2014-01-17 16:25	11K
	Data.Nat.html	2014-01-17 16:25	123K
	Data.Plus.html	2014-01-17 16:25	50K
	Data.Product.N-ary.html	2014-01-17 16:25	39K
	Data.Product.html	2014-01-17 16:25	94K
	Data.Rational.html	2014-01-17 16:25	111K
	Data.ReflexiveClosur..>	2014-01-17 16:25	26K
	Data.Sign.Properties..>	2014-01-17 16:25	10K
	Data.Sign.html	2014-01-17 16:25	11K
	Data.Star.BoundedVec..>	2014-01-17 16:25	25K
	Data.Star.Decoration..>	2014-01-17 16:25	73K
	Data.Star.Environmen..>	2014-01-17 16:25	17K
	Data.Star.Fin.html	2014-01-17 16:25	8.0K
	Data.Star.List.html	2014-01-17 16:25	8.7K
	Data.Star.Nat.html	2014-01-17 16:25	18K
	Data.Star.Pointer.html	2014-01-17 16:25	72K
	Data.Star.Properties..>	2014-01-17 16:25	98K
	Data.Star.Vec.html	2014-01-17 16:25	28K
	Data.Star.html	2014-01-17 16:25	98K
	Data.Stream.html	2014-01-17 16:25	100K
	Data.String.html	2014-01-17 16:25	39K
	Data.Sum.html	2014-01-17 16:25	37K
	Data.Unit.Core.html	2014-01-17 16:25	12K
	Data.Unit.html	2014-01-17 16:25	22K
	Data.Vec.Equality.html	2014-01-17 16:25	68K
	Data.Vec.N-ary.html	2014-01-17 16:25	162K
	Data.Vec.Properties...>	2014-01-17 16:25	338K
	Data.Vec.html	2014-01-17 16:25	203K
	Data.W.html	2014-01-17 16:25	17K
	Everything.html	2014-01-17 16:25	65K
	Foreign.Haskell.html	2014-01-17 16:25	2.6K
	Function.Bijection.html	2014-01-17 16:25	40K
	Function.Equality.html	2014-01-17 16:25	56K
	Function.Equivalence..>	2014-01-17 16:25	65K
	Function.Injection.html	2014-01-17 16:25	30K
	Function.Inverse.html	2014-01-17 16:25	86K
	Function.LeftInverse..>	2014-01-17 16:25	62K
	Function.Related.Typ..>	2014-01-17 16:25	378K
	Function.Related.html	2014-01-17 16:25	208K
	Function.Surjection...>	2014-01-17 16:25	46K
	Function.html	2014-01-17 16:25	70K
	IO.Primitive.html	2014-01-17 16:25	19K
	IO.html	2014-01-17 16:25	58K
	Induction.Lexicograp..>	2014-01-17 16:25	54K
	Induction.Nat.html	2014-01-17 16:25	109K
	Induction.WellFounde..>	2014-01-17 16:25	96K
	Induction.html	2014-01-17 16:25	31K
	Irrelevance.html	2014-01-17 16:25	3.9K
	Level.html	2014-01-17 16:25	5.2K
	Record.html	2014-01-17 16:25	146K
	Reflection.html	2014-01-17 16:25	231K
	Relation.Binary.Cons..>	2014-01-17 16:25	11K
	Relation.Binary.Cons..>	2014-01-17 16:25	87K
	Relation.Binary.Core..>	2014-01-17 16:25	131K
	Relation.Binary.EqRe..>	2014-01-17 16:25	6.7K
	Relation.Binary.Flip..>	2014-01-17 16:25	148K
	Relation.Binary.Hete..>	2014-01-17 16:25	9.5K
	Relation.Binary.Hete..>	2014-01-17 16:25	155K
	Relation.Binary.Inde..>	2014-01-17 16:25	40K
	Relation.Binary.Inde..>	2014-01-17 16:25	15K
	Relation.Binary.Indu..>	2014-01-17 16:25	20K
	Relation.Binary.List..>	2014-01-17 16:25	100K
	Relation.Binary.List..>	2014-01-17 16:25	172K
	Relation.Binary.List..>	2014-01-17 16:25	238K
	Relation.Binary.NonS..>	2014-01-17 16:25	63K
	Relation.Binary.On.html	2014-01-17 16:25	152K
	Relation.Binary.Orde..>	2014-01-17 16:25	30K
	Relation.Binary.Part..>	2014-01-17 16:25	4.6K
	Relation.Binary.Preo..>	2014-01-17 16:25	23K
	Relation.Binary.Prod..>	2014-01-17 16:25	120K
	Relation.Binary.Prod..>	2014-01-17 16:25	334K
	Relation.Binary.Prod..>	2014-01-17 16:25	224K
	Relation.Binary.Prop..>	2014-01-17 16:25	17K
	Relation.Binary.Prop..>	2014-01-17 16:25	7.1K
	Relation.Binary.Prop..>	2014-01-17 16:25	113K
	Relation.Binary.Prop..>	2014-01-17 16:25	9.0K
	Relation.Binary.Prop..>	2014-01-17 16:25	8.5K
	Relation.Binary.Prop..>	2014-01-17 16:25	9.2K
	Relation.Binary.Prop..>	2014-01-17 16:25	9.6K
	Relation.Binary.Prop..>	2014-01-17 16:25	9.7K
	Relation.Binary.Prop..>	2014-01-17 16:25	7.4K
	Relation.Binary.Refl..>	2014-01-17 16:25	60K
	Relation.Binary.Sigm..>	2014-01-17 16:25	364K
	Relation.Binary.Simp..>	2014-01-17 16:25	14K
	Relation.Binary.Stri..>	2014-01-17 16:25	5.1K
	Relation.Binary.Stri..>	2014-01-17 16:25	67K
	Relation.Binary.Sum...>	2014-01-17 16:25	491K
	Relation.Binary.Vec...>	2014-01-17 16:25	188K
	Relation.Binary.html	2014-01-17 16:25	139K
	Relation.Nullary.Cor..>	2014-01-17 16:25	7.5K
	Relation.Nullary.Dec..>	2014-01-17 16:25	66K
	Relation.Nullary.Imp..>	2014-01-17 16:25	9.6K
	Relation.Nullary.Neg..>	2014-01-17 16:25	126K
	Relation.Nullary.Pro..>	2014-01-17 16:25	9.1K
	Relation.Nullary.Sum..>	2014-01-17 16:25	16K
	Relation.Nullary.Uni..>	2014-01-17 16:25	111K
	Relation.Nullary.html	2014-01-17 16:25	3.6K
	Relation.Unary.html	2014-01-17 16:25	69K
	Size.html	2014-01-17 16:25	3.6K
	Universe.html	2014-01-17 16:25	11K

module README where

------------------------------------------------------------------------
-- The Agda standard library
--
-- Author: Nils Anders Danielsson, with contributions from Andreas
-- Abel, Stevan Andjelkovic, Jean-Philippe Bernardy, Peter Berry,
-- Joachim Breitner, Samuel Bronson, Daniel Brown, Liang-Ting Chen,
-- Dominique Devriese, Dan Doel, Érdi Gergő, Helmut Grohne, Simon
-- Foster, Liyang Hu, Patrik Jansson, Alan Jeffrey, Eric Mertens,
-- Darin Morrison, Guilhem Moulin, Shin-Cheng Mu, Ulf Norell, Noriyuki
-- OHKAWA, Nicolas Pouillard, Andrés Sicard-Ramírez and Noam
-- Zeilberger
------------------------------------------------------------------------

-- Note that the development version of the library often requires the
-- latest development version of Agda.

-- Note also 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).

-- To compile the library using the MAlonzo compiler you first need to
-- install some supporting Haskell code, for instance as follows:
--
--   cd ffi
--   cabal install
--
-- Currently the library does not support the Epic or JavaScript
-- compiler backends.

-- 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.
-- • Irrelevance
--     Definitions related to (proscriptive) irrelevance.
-- • Level
--     Universe levels.
-- • Record
--     An encoding of record types with manifest fields and "with".
-- • 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/integers and some
-- related operations and properties are defined, and how they can be
-- used:

import README.Nat
import README.Integer

-- Some examples showing how the AVL tree module can be used.

import README.AVL

-- An example showing how the Record module can be used.

import README.Record

-- An example showing how the case expression can be used.

import README.Case

------------------------------------------------------------------------
-- 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

-- Note that the Everything module is generated automatically. If you
-- have downloaded the library from its darcs repository and want to
-- type check README then you can (try to) construct Everything by
-- running "cabal install && GenerateEverything".

-- Note that all library sources are located under src or ffi. The
-- modules README, README.* and Everything are not really part of the
-- library, so these modules are located in the top-level directory
-- instead.