Index of /~nad/listings/lib-0.1

[ICO]NameLast modifiedSizeDescription

[PARENTDIR]Parent Directory   -  
[TXT]Agda.css 2009-04-23 17:30 1.0K 
[TXT]Data.Empty1.html 2009-04-23 17:30 1.7K 
[TXT]Data.Unit1.html 2009-04-23 17:30 1.7K 
[TXT]Data.Empty.html 2009-04-23 17:30 2.8K 
[TXT]Size.html 2009-04-23 17:30 3.4K 
[TXT]Data.Bool.Show.html 2009-04-23 17:30 3.4K 
[TXT]Data.Maybe.Core.html 2009-04-23 17:30 3.7K 
[TXT]Relation.Binary.Part..>2009-04-23 17:30 3.9K 
[TXT]Algebra.RingSolver.S..>2009-04-23 17:30 4.1K 
[TXT]Relation.Binary.Stri..>2009-04-23 17:30 4.7K 
[TXT]Category.Monad.Ident..>2009-04-23 17:30 5.1K 
[TXT]Relation.Binary.EqRe..>2009-04-23 17:30 5.4K 
[TXT]Relation.Nullary.Cor..>2009-04-23 17:30 6.3K 
[TXT]Category.Applicative..>2009-04-23 17:30 6.3K 
[TXT]Relation.Binary.Prop..>2009-04-23 17:30 6.8K 
[TXT]Category.Functor.html 2009-04-23 17:30 7.1K 
[TXT]Relation.Binary.Prop..>2009-04-23 17:30 7.9K 
[TXT]Relation.Nullary.Pro..>2009-04-23 17:30 8.3K 
[TXT]Relation.Binary.Prop..>2009-04-23 17:30 8.4K 
[TXT]Data.Star.Fin.html 2009-04-23 17:30 8.7K 
[TXT]Relation.Binary.Simp..>2009-04-23 17:30 8.8K 
[TXT]Coinduction.html 2009-04-23 17:30 8.9K 
[TXT]Data.Star.List.html 2009-04-23 17:30 9.3K 
[TXT]Relation.Binary.Prop..>2009-04-23 17:30 9.5K 
[TXT]Relation.Binary.Cons..>2009-04-23 17:30 9.6K 
[TXT]Relation.Binary.Prop..>2009-04-23 17:30 9.6K 
[TXT]Data.Conat.html 2009-04-23 17:30 10K 
[TXT]Induction1.Nat.html 2009-04-23 17:30 11K 
[TXT]Data.Nat.Show.html 2009-04-23 17:30 11K 
[TXT]Data.Sign.html 2009-04-23 17:30 11K 
[TXT]Data.DifferenceNat.html2009-04-23 17:30 12K 
[TXT]Relation.Unary1.html 2009-04-23 17:30 12K 
[TXT]Foreign.Haskell.html 2009-04-23 17:30 13K 
[TXT]Category.Monad.html 2009-04-23 17:30 14K 
[TXT]Relation.Binary.Prop..>2009-04-23 17:30 14K 
[TXT]IO.Primitive.html 2009-04-23 17:30 14K 
[TXT]Relation.Nullary.Sum..>2009-04-23 17:30 14K 
[TXT]Data.Char.html 2009-04-23 17:30 15K 
[TXT]Induction.WellFounde..>2009-04-23 17:30 16K 
[TXT]Induction1.WellFound..>2009-04-23 17:30 16K 
[TXT]Relation.Nullary.Dec..>2009-04-23 17:30 17K 
[TXT]Data.BoundedVec.Inef..>2009-04-23 17:30 18K 
[TXT]Data.Star.Nat.html 2009-04-23 17:30 18K 
[TXT]Data.Star.Environmen..>2009-04-23 17:30 19K 
[TXT]Relation.Binary.Orde..>2009-04-23 17:30 19K 
[TXT]Data.Cofin.html 2009-04-23 17:30 19K 
[TXT]Algebra.Props.Lattic..>2009-04-23 17:30 20K 
[TXT]Data.Unit.html 2009-04-23 17:30 22K 
[TXT]Data.Vec1.html 2009-04-23 17:30 23K 
[TXT]Relation.Binary.Preo..>2009-04-23 17:30 23K 
[TXT]Category.Applicative..>2009-04-23 17:30 23K 
[TXT]Data.Vec.Properties...>2009-04-23 17:30 23K 
[TXT]Induction1.html 2009-04-23 17:30 24K 
[TXT]Induction.html 2009-04-23 17:30 24K 
[TXT]Data.AVL.Sets.html 2009-04-23 17:30 24K 
[TXT]Algebra.Morphism.html 2009-04-23 17:30 25K 
[TXT]Relation.Nullary.html 2009-04-23 17:30 25K 
[TXT]Data.String.html 2009-04-23 17:30 25K 
[TXT]Data.Sum.html 2009-04-23 17:30 26K 
[TXT]Data.Fin.Subset.html 2009-04-23 17:30 27K 
[TXT]Data.Star.BoundedVec..>2009-04-23 17:30 28K 
[TXT]Data.Bool.html 2009-04-23 17:30 29K 
[TXT]Data.Star.Vec.html 2009-04-23 17:30 30K 
[TXT]Data.List1.html 2009-04-23 17:30 31K 
[TXT]Algebra.Operations.html2009-04-23 17:30 31K 
[TXT]Category.Monad.Index..>2009-04-23 17:30 32K 
[TXT]Data.DifferenceList...>2009-04-23 17:30 33K 
[TXT]Algebra.Props.Abelia..>2009-04-23 17:30 34K 
[TXT]Relation.Unary.html 2009-04-23 17:30 35K 
[TXT]Data.DifferenceVec.html2009-04-23 17:30 35K 
[TXT]Relation.Binary.Prop..>2009-04-23 17:30 35K 
[TXT]Data.BoundedVec.html 2009-04-23 17:30 37K 
[TXT]Induction.Lexicograp..>2009-04-23 17:30 38K 
[TXT]Algebra.Props.Group...>2009-04-23 17:30 38K 
[TXT]Category.Monad.Conti..>2009-04-23 17:30 38K 
[TXT]Relation.Binary.Prop..>2009-04-23 17:30 40K 
[TXT]Algebra.Props.Ring.html2009-04-23 17:30 42K 
[TXT]Data.List.Equality.html2009-04-23 17:30 42K 
[TXT]Data.List.NonEmpty.P..>2009-04-23 17:30 42K 
[TXT]Data.Nat.Coprimality..>2009-04-23 17:30 44K 
[TXT]Relation.Binary.Refl..>2009-04-23 17:30 44K 
[TXT]Data.AVL.IndexedMap...>2009-04-23 17:30 45K 
[TXT]Data.Product.Record...>2009-04-23 17:30 45K 
[TXT]Induction.Nat.html 2009-04-23 17:30 45K 
[TXT]Algebra.Props.Distri..>2009-04-23 17:30 46K 
[TXT]Algebra.RingSolver.A..>2009-04-23 17:30 47K 
[TXT]IO.html 2009-04-23 17:30 48K 
[TXT]Data.Fin.Subset.Prop..>2009-04-23 17:30 48K 
[TXT]Relation.Binary.NonS..>2009-04-23 17:30 48K 
[TXT]Category.Monad.Parti..>2009-04-23 17:30 49K 
[TXT]Relation.Binary.Func..>2009-04-23 17:30 51K 
[TXT]Data.Product1.html 2009-04-23 17:30 52K 
[TXT]Algebra.FunctionProp..>2009-04-23 17:30 55K 
[TXT]Data.Sets.html 2009-04-23 17:30 56K 
[TXT]Data.Map.html 2009-04-23 17:30 56K 
[TXT]Data.Digit.html 2009-04-23 17:30 61K 
[TXT]Data.Product.html 2009-04-23 17:30 63K 
[TXT]Relation.Nullary.Neg..>2009-04-23 17:30 65K 
[TXT]Data.Vec.N-ary1.html 2009-04-23 17:30 67K 
[TXT]Data.Vec.Equality.html 2009-04-23 17:30 67K 
[TXT]Relation.Binary.Stri..>2009-04-23 17:30 67K 
[TXT]Data.Function.html 2009-04-23 17:30 68K 
[TXT]Data.Star.Pointer.html 2009-04-23 17:30 71K 
[TXT]Category.Monad.State..>2009-04-23 17:30 71K 
[TXT]Data.Star.Decoration..>2009-04-23 17:30 72K 
[TXT]Data.Fin.html 2009-04-23 17:30 72K 
[TXT]Data.Stream.html 2009-04-23 17:30 72K 
[TXT]Data.Maybe.html 2009-04-23 17:30 74K 
[TXT]Everything.html 2009-04-23 17:30 76K 
[TXT]Data.Star.html 2009-04-23 17:30 76K 
[TXT]Data.Nat.DivMod.html 2009-04-23 17:30 77K 
[TXT]Data.Vec.N-ary.html 2009-04-23 17:30 78K 
[TXT]Relation.Binary.On.html2009-04-23 17:30 84K 
[TXT]Relation.Binary.Cons..>2009-04-23 17:30 84K 
[TXT]Relation.Binary.html 2009-04-23 17:30 84K 
[TXT]Relation.Binary.Hete..>2009-04-23 17:30 89K 
[TXT]Data.Nat.Divisibilit..>2009-04-23 17:30 89K 
[TXT]Data.Star.Properties..>2009-04-23 17:30 91K 
[TXT]Data.Nat.GCD.html 2009-04-23 17:30 92K 
[TXT]Relation.Binary.Core..>2009-04-23 17:30 98K 
[TXT]Data.List.NonEmpty.html2009-04-23 17:30 107K 
[TXT]Data.Nat.html 2009-04-23 17:30 113K 
[TXT]Data.Fin.Props.html 2009-04-23 17:30 115K 
[TXT]Relation.Binary.Prod..>2009-04-23 17:30 117K 
[TXT]Relation.Nullary.Uni..>2009-04-23 17:30 118K 
[TXT]Relation.Binary.Flip..>2009-04-23 17:30 120K 
[TXT]Data.Colist.html 2009-04-23 17:30 121K 
[TXT]Data.Covec.html 2009-04-23 17:30 122K 
[TXT]Data.Fin.Dec.html 2009-04-23 17:30 128K 
[TXT]Data.Bool.Properties..>2009-04-23 17:30 128K 
[TXT]Algebra.Structures.html2009-04-23 17:30 129K 
[TXT]Algebra.html 2009-04-23 17:30 135K 
[TXT]Algebra.RingSolver.L..>2009-04-23 17:30 143K 
[TXT]Relation.Binary.Prod..>2009-04-23 17:30 151K 
[TXT]Data.Vec.html 2009-04-23 17:30 164K 
[TXT]Data.Integer.html 2009-04-23 17:30 170K 
[TXT]Data.Bin.html 2009-04-23 17:30 170K 
[TXT]Algebra.RingSolver.html2009-04-23 17:30 192K 
[TXT]Relation.Binary.Prod..>2009-04-23 17:30 194K 
[TXT]Data.Graph.Acyclic.html2009-04-23 17:30 197K 
[TXT]Data.AVL.html 2009-04-23 17:30 214K 
[TXT]Data.List.html 2009-04-23 17:30 221K 
[TXT]Relation.Binary.Sum...>2009-04-23 17:30 271K 
[TXT]Data.List.Properties..>2009-04-23 17:30 302K 
[TXT]Data.Nat.Properties...>2009-04-23 17:30 407K 
[TXT]Algebra.Props.Boolea..>2009-04-23 17:30 492K 

README
module README where

------------------------------------------------------------------------
-- The Agda "standard" library, version 0.1
------------------------------------------------------------------------

-- This release has been tested using Agda 2.2.2.

-- Note that no guarantees are currently made about forwards or
-- backwards compatibility.

-- To make use of the library, add the path to the library’s root
-- directory 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 programs using some of the IO functions you need to
-- install the Haskell package utf8-string (available from Hackage).

-- Contributions to this library are welcome. 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.

------------------------------------------------------------------------
-- 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. (Also some
--     combinators working solely on and with functions; see
--     Data.Function.)
-- • Foreign
--     Related to the foreign function interface.
-- • Induction
--     A general framework for induction (includes lexicographic and
--     well-founded induction).
-- • IO
--     Input/output-related functions.
-- • Relation
--     Properties of and proofs about relations (mostly homogeneous
--     binary relations).
-- • Size
--     Sizes used by the sized types mechanism.

------------------------------------------------------------------------
-- 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.:
--
--   module Algebra.Structures (S : Setoid) where
--
--   ⋮
--
--   record IsSemigroup (∙ : Op₂) : Set where
--     field
--       assoc    : Associative ∙
--       ∙-pres-≈ : ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
--
-- More specific concepts are then specified in terms of the simpler ones:
--
--   record IsMonoid (∙ : Op₂) (ε : carrier) : Set where
--     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 _∼_
--       ≈-resp-∼      : _≈_ Respects₂ _∼_
--
--     module Eq = IsEquivalence isEquivalence
--
--     refl : Reflexive _∼_
--     refl = reflexive Eq.refl
--
-- 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 : Set1 where
--     infixl 7 _∙_
--     field
--       setoid      : Setoid
--       _∙_         : P.Op₂ setoid
--       isSemigroup : IsSemigroup setoid _∙_
--
--     open Setoid setoid public
--     open IsSemigroup setoid isSemigroup public
--
--   record Monoid : Set1 where
--     infixl 7 _∙_
--     field
--       setoid   : Setoid
--       _∙_      : P.Op₂ setoid
--       ε        : Setoid.carrier setoid
--       isMonoid : IsMonoid setoid _∙_ ε
--
--     open Setoid setoid public
--     open IsMonoid setoid isMonoid public
--
--     semigroup : Semigroup
--     semigroup = record { isSemigroup = isSemigroup }
--
-- 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.

------------------------------------------------------------------------
-- Core modules
------------------------------------------------------------------------

-- Some modules have names ending in ".Core". These modules are
-- internal, and have 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