------------------------------------------------------------------------ -- The Agda standard library -- -- All library modules, along with short descriptions ------------------------------------------------------------------------ -- Note that core modules are not included. module Everything where -- Definitions of algebraic structures like monoids and rings -- (packed in records together with sets, operations, etc.) import Algebra -- Properties of functions, such as associativity and commutativity import Algebra.FunctionProperties -- Morphisms between algebraic structures import Algebra.Morphism -- Some defined operations (multiplication by natural number and -- exponentiation) import Algebra.Operations -- Some derivable properties import Algebra.Props.AbelianGroup -- Some derivable properties import Algebra.Props.BooleanAlgebra -- Boolean algebra expressions import Algebra.Props.BooleanAlgebra.Expression -- Some derivable properties import Algebra.Props.DistributiveLattice -- Some derivable properties import Algebra.Props.Group -- Some derivable properties import Algebra.Props.Lattice -- Some derivable properties import Algebra.Props.Ring -- Solver for commutative ring or semiring equalities import Algebra.RingSolver -- Commutative semirings with some additional structure ("almost" -- commutative rings), used by the ring solver import Algebra.RingSolver.AlmostCommutativeRing -- Some boring lemmas used by the ring solver import Algebra.RingSolver.Lemmas -- Instantiates the ring solver with two copies of the same ring import Algebra.RingSolver.Simple -- Some algebraic structures (not packed up with sets, operations, -- etc.) import Algebra.Structures -- Applicative functors import Category.Applicative -- Indexed applicative functors import Category.Applicative.Indexed -- Functors import Category.Functor -- Monads import Category.Monad -- A delimited continuation monad import Category.Monad.Continuation -- The identity monad import Category.Monad.Identity -- Indexed monads import Categor