------------------------------------------------------------------------
-- The Agda standard library
--
-- All library modules, along with short descriptions
------------------------------------------------------------------------

-- Note that core modules are not included.

{-# OPTIONS --safe --guardedness #-}

module EverythingSafe where

-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
import Algebra

-- Algebraic objects with an apartness relation
import Algebra.Apartness

-- Bundles for local algebraic structures
import Algebra.Apartness.Bundles

-- Properties of Heyting Commutative Rings
import Algebra.Apartness.Properties.HeytingCommutativeRing

-- Algebraic structures with an apartness relation
import Algebra.Apartness.Structures

-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
import Algebra.Bundles

-- Definitions of 'raw' bundles
import Algebra.Bundles.Raw

-- Lemmas relating algebraic definitions (such as associativity and
-- commutativity) that don't require the equality relation to be a setoid.
import Algebra.Consequences.Base

-- Relations between properties of functions, such as associativity and
-- commutativity (specialised to propositional equality)
import Algebra.Consequences.Propositional

-- Relations between properties of functions, such as associativity and
-- commutativity, when the underlying relation is a setoid
import Algebra.Consequences.Setoid

-- Definition of algebraic structures we get from freely adding an
-- identity element
import Algebra.Construct.Add.Identity

-- Instances of algebraic structures made by taking two other instances
-- A and B, and having elements of the new instance be pairs |A| × |B|.
-- In mathematics, this would usually be written A × B or A ⊕ B.
import Algebra.Construct.DirectProduct

-- Flipping the arguments of a binary operation preserves many of its
-- algebraic properties.
import Algebra.Construct.Flip.Op

-- Instances of algebraic structures where the carrier is ⊥.
-- In mathematics, this is usually called 0.
import Algebra.Construct.Initial

-- Definitions of the lexicographic product of two operators.
import Algebra.Construct.LexProduct

-- Definitions of the lexicographic product of two operators.
import Algebra.Construct.LexProduct.Base

-- Properties of the inner lexicographic product of two operators.
import Algebra.Construct.LexProduct.Inner

-- Choosing between elements based on the result of applying a function
import Algebra.Construct.LiftedChoice

-- Basic definition of an operator that computes the min/max value
-- with respect to a total preorder.
import Algebra.Construct.NaturalChoice.Base

-- The max operator derived from an arbitrary total preorder.
import Algebra.Construct.NaturalChoice.Max

-- Properties of a max operator derived from a spec over a total
-- preorder.
import Algebra.Construct.NaturalChoice.MaxOp

-- The min operator derived from an arbitrary total preorder.
import Algebra.Construct.NaturalChoice.Min

-- Properties of min and max operators specified over a total
-- preorder.
import Algebra.Construct.NaturalChoice.MinMaxOp

-- Properties of a min operator derived from a spec over a total
-- preorder.
import Algebra.Construct.NaturalChoice.MinOp

-- For each `IsX` algebraic structure `S`, lift the structure to the
-- 'pointwise' function space `A → S`: categorically, this is the
-- *power* object in the relevant category of `X` objects and morphisms
import Algebra.Construct.Pointwise

-- Substituting equalities for binary relations
import Algebra.Construct.Subst.Equality

-- Instances of algebraic structures where the carrier is ⊤. In
-- mathematics, this is usually called 0 (1 in the case of Monoid, Group).
import Algebra.Construct.Terminal

-- Instances of algebraic structures where the carrier is ⊤. In
-- mathematics, this is usually called 0 (1 in the case of Monoid, Group).
import Algebra.Construct.Zero

-- Properties of functions, such as associativity and commutativity
import Algebra.Definitions

-- Basic auxiliary definitions for magma-like structures
import Algebra.Definitions.RawMagma

-- Basic auxiliary definitions for monoid-like structures
import Algebra.Definitions.RawMonoid

-- Basic auxiliary definitions for semiring-like structures
import Algebra.Definitions.RawSemiring

-- Definitions of algebraic structures like semilattices and lattices
-- (packed in records together with sets, operations, etc.), defined via
-- meet/join operations and their properties
import Algebra.Lattice

-- Definitions of algebraic structures like semilattices and lattices
-- (packed in records together with sets, operations, etc.), defined via
-- meet/join operations and their properties
import Algebra.Lattice.Bundles

-- Definitions of 'raw' bundles
import Algebra.Lattice.Bundles.Raw

-- Instances of algebraic structures made by taking two other instances
-- A and B, and having elements of the new instance be pairs |A| × |B|.
-- In mathematics, this would usually be written A × B or A ⊕ B.
import Algebra.Lattice.Construct.DirectProduct

-- Choosing between elements based on the result of applying a function
import Algebra.Lattice.Construct.LiftedChoice

-- Properties of a max operator derived from a spec over a total
-- preorder.
import Algebra.Lattice.Construct.NaturalChoice.MaxOp

-- Properties of min and max operators specified over a total preorder.
import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp

-- Properties of a min operator derived from a spec over a total
-- preorder.
import Algebra.Lattice.Construct.NaturalChoice.MinOp

-- Substituting equalities for binary relations
import Algebra.Lattice.Construct.Subst.Equality

-- Instances of algebraic lattice structures where the carrier is ⊤.
-- In mathematics, this is usually called 0.
import Algebra.Lattice.Construct.Zero

-- Morphisms between algebraic lattice structures
import Algebra.Lattice.Morphism

-- The composition of morphisms between algebraic lattice structures.
import Algebra.Lattice.Morphism.Construct.Composition

-- The identity morphism for algebraic lattice structures
import Algebra.Lattice.Morphism.Construct.Identity

-- Consequences of a monomorphism between lattice-like structures
import Algebra.Lattice.Morphism.LatticeMonomorphism

-- Morphisms between algebraic lattice structures
import Algebra.Lattice.Morphism.Structures

-- Some derivable properties of Boolean algebras
import Algebra.Lattice.Properties.BooleanAlgebra

-- Boolean algebra expressions
import Algebra.Lattice.Properties.BooleanAlgebra.Expression

-- Some derivable properties
import Algebra.Lattice.Properties.DistributiveLattice

-- Some derivable properties of lattices
import Algebra.Lattice.Properties.Lattice

-- Some derivable properties of semilattices
import Algebra.Lattice.Properties.Semilattice

-- Some lattice-like structures defined by properties of _∧_ and _∨_
-- (not packed up with sets, operations, etc.)
import Algebra.Lattice.Structures

-- Some biased records for lattice-like structures. Such records are
-- often easier to construct, but are suboptimal to use more widely and
-- should be converted to the standard record definitions immediately
-- using the provided conversion functions.
import Algebra.Lattice.Structures.Biased

-- Definitions of algebraic structure module
-- packed in records together with sets, operations, etc.
import Algebra.Module

-- Definitions of algebraic structures defined over some other
-- structure, like modules and vector spaces
import Algebra.Module.Bundles

-- Definitions of 'raw' bundles for module-like algebraic structures
import Algebra.Module.Bundles.Raw

-- Relations between properties of scaling and other operations
import Algebra.Module.Consequences

-- This module constructs the biproduct of two R-modules, and similar
-- for weaker module-like structures.
-- The intended universal property is that the biproduct is both a
-- product and a coproduct in the category of R-modules.
import Algebra.Module.Construct.DirectProduct

-- The non-commutative analogue of Nagata's construction of
-- the "idealization of a module", (Local Rings, 1962; Wiley)
-- defined here on R-R-*bi*modules M over a ring R, as used in
-- "Forward- or reverse-mode automatic differentiation: What's the difference?"
-- (Van den Berg, Schrijvers, McKinna, Vandenbroucke;
-- Science of Computer Programming, Vol. 234, January 2024
-- https://doi.org/10.1016/j.scico.2023.103010)
import Algebra.Module.Construct.Idealization

-- This module constructs the unit of the monoidal structure on
-- R-modules, and similar for weaker module-like structures.
-- The intended universal property is that the maps out of the tensor
-- unit into M are isomorphic to the elements of M.
import Algebra.Module.Construct.TensorUnit

-- This module constructs the zero R-module, and similar for weaker
-- module-like structures.
-- The intended universal property is that, given any R-module M, there
-- is a unique map into and a unique map out of the zero R-module
-- from/to M.
import Algebra.Module.Construct.Zero

-- This module collects the property definitions for left-scaling
-- (LeftDefs), right-scaling (RightDefs), and both (BiDefs).
import Algebra.Module.Definitions

-- Properties connecting left-scaling and right-scaling
import Algebra.Module.Definitions.Bi

-- Properties connecting left-scaling and right-scaling over the same scalars
import Algebra.Module.Definitions.Bi.Simultaneous

-- Properties of left-scaling
import Algebra.Module.Definitions.Left

-- Properties of right-scaling
import Algebra.Module.Definitions.Right

-- Properties of a monomorphism between bimodules
import Algebra.Module.Morphism.BimoduleMonomorphism

-- Consequences of a monomorphism between bisemimodules
import Algebra.Module.Morphism.BisemimoduleMonomorphism

-- The composition of morphisms between module-like algebraic structures.
import Algebra.Module.Morphism.Construct.Composition

-- The identity morphism for module-like algebraic structures
import Algebra.Module.Morphism.Construct.Identity

-- Basic definitions for morphisms between module-like algebraic
-- structures
import Algebra.Module.Morphism.Definitions

-- Consequences of a monomorphism between left modules
import Algebra.Module.Morphism.LeftModuleMonomorphism

-- Consequences of a monomorphism between left semimodules
import Algebra.Module.Morphism.LeftSemimoduleMonomorphism

-- Properties of linear maps.
import Algebra.Module.Morphism.ModuleHomomorphism

-- Consequences of a monomorphism between modules
import Algebra.Module.Morphism.ModuleMonomorphism

-- Consequences of a monomorphism between right modules
import Algebra.Module.Morphism.RightModuleMonomorphism

-- Consequences of a monomomorphism between right semimodules
import Algebra.Module.Morphism.RightSemimoduleMonomorphism

-- Properties of a monomorphism between semimodules
import Algebra.Module.Morphism.SemimoduleMonomorphism

-- Morphisms between module-like algebraic structures
import Algebra.Module.Morphism.Structures

-- Properties of modules.
import Algebra.Module.Properties

-- Properties of semimodules.
import Algebra.Module.Properties.Semimodule

-- Some algebraic structures defined over some other structure
import Algebra.Module.Structures

-- This module provides alternative ways of providing instances of
-- structures in the Algebra.Module hierarchy.
import Algebra.Module.Structures.Biased

-- Morphisms between algebraic structures
import Algebra.Morphism

-- Bundled definitions of homomorphisms between algebras
import Algebra.Morphism.Bundles

-- Some properties of Magma homomorphisms
import Algebra.Morphism.Consequences

-- The composition of morphisms between algebraic structures.
import Algebra.Morphism.Construct.Composition

-- The identity morphism for algebraic structures
import Algebra.Morphism.Construct.Identity

-- The unique morphism from the initial object,
-- for each of the relevant categories. Since
-- `Semigroup` and `Band` are simply `Magma`s
-- satisfying additional properties, it suffices to
-- define the morphism on the underlying `RawMagma`.
import Algebra.Morphism.Construct.Initial

-- The unique morphism to the terminal object,
-- for each of the relevant categories. Since
-- each terminal algebra builds on `Monoid`,
-- possibly with additional (trivial) operations,
-- satisfying additional properties, it suffices to
-- define the morphism on the underlying `RawMonoid`
import Algebra.Morphism.Construct.Terminal

-- Basic definitions for morphisms between algebraic structures
import Algebra.Morphism.Definitions

-- Consequences of a monomorphism between group-like structures
import Algebra.Morphism.GroupMonomorphism

-- Consequences of a monomorphism between magma-like structures
import Algebra.Morphism.MagmaMonomorphism

-- Consequences of a monomorphism between monoid-like structures
import Algebra.Morphism.MonoidMonomorphism

-- Consequences of a monomorphism between ring-like structures
import Algebra.Morphism.RingMonomorphism

-- Morphisms between algebraic structures
import Algebra.Morphism.Structures

-- Some derivable properties
import Algebra.Properties.AbelianGroup

-- Some properties of operations in CancellativeCommutativeSemiring.
import Algebra.Properties.CancellativeCommutativeSemiring

-- Properties of divisibility over commutative magmas
import Algebra.Properties.CommutativeMagma.Divisibility

-- Some derivable properties
import Algebra.Properties.CommutativeMonoid

-- Multiplication over a monoid (i.e. repeated addition)
import Algebra.Properties.CommutativeMonoid.Mult

-- Multiplication over a monoid (i.e. repeated addition) optimised for
-- type checking.
import Algebra.Properties.CommutativeMonoid.Mult.TCOptimised

-- Finite summations over a commutative monoid
import Algebra.Properties.CommutativeMonoid.Sum

-- Some theory for commutative semigroup
import Algebra.Properties.CommutativeSemigroup

-- Properties of divisibility over commutative semigroups
import Algebra.Properties.CommutativeSemigroup.Divisibility

-- The Binomial Theorem for Commutative Semirings
import Algebra.Properties.CommutativeSemiring.Binomial

-- Exponentiation defined over a commutative semiring as repeated multiplication
import Algebra.Properties.CommutativeSemiring.Exp

-- Exponentiation over a semiring optimised for type-checking.
import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised

-- Some derivable properties
import Algebra.Properties.Group

-- Some derivable properties
import Algebra.Properties.IdempotentCommutativeMonoid

-- Some derivable properties
import Algebra.Properties.KleeneAlgebra

-- Some basic properties of Loop
import Algebra.Properties.Loop

-- Divisibility over magmas
import Algebra.Properties.Magma.Divisibility

-- Some basic properties of Quasigroup
import Algebra.Properties.MiddleBolLoop

-- Properties of divisibility over monoids
import Algebra.Properties.Monoid.Divisibility

-- Multiplication over a monoid (i.e. repeated addition)
import Algebra.Properties.Monoid.Mult

-- Multiplication over a monoid (i.e. repeated addition) optimised for
-- type checking.
import Algebra.Properties.Monoid.Mult.TCOptimised

-- Finite summations over a monoid
import Algebra.Properties.Monoid.Sum

-- Some derivable properties
import Algebra.Properties.MoufangLoop

-- Some basic properties of Quasigroup
import Algebra.Properties.Quasigroup

-- Some basic properties of Rings
import Algebra.Properties.Ring

-- Some basic properties of RingWithoutOne
import Algebra.Properties.RingWithoutOne

-- Some theory for Semigroup
import Algebra.Properties.Semigroup

-- Properties of divisibility over semigroups
import Algebra.Properties.Semigroup.Divisibility

-- The Binomial Theorem for *-commuting elements in a Semiring
import Algebra.Properties.Semiring.Binomial

-- Properties of divisibility over semirings
import Algebra.Properties.Semiring.Divisibility

-- Exponentiation defined over a semiring as repeated multiplication
import Algebra.Properties.Semiring.Exp

-- Exponentiation over a semiring optimised for type-checking.
import Algebra.Properties.Semiring.Exp.TCOptimised

-- Exponentiation over a semiring optimised for tail-recursion.
import Algebra.Properties.Semiring.Exp.TailRecursiveOptimised

-- Multiplication by a natural number over a semiring
import Algebra.Properties.Semiring.Mult

-- Multiplication over a semiring optimised for type-checking.
import Algebra.Properties.Semiring.Mult.TCOptimised

-- Some theory for CancellativeCommutativeSemiring.
import Algebra.Properties.Semiring.Primality

-- Finite summations over a semiring
import Algebra.Properties.Semiring.Sum

-- Solver for equations in commutative monoids
import Algebra.Solver.CommutativeMonoid

-- An example of how Algebra.CommutativeMonoidSolver can be used
import Algebra.Solver.CommutativeMonoid.Example

-- Normal forms in commutative monoids
import Algebra.Solver.CommutativeMonoid.Normal

-- Solver for equations in idempotent commutative monoids
import Algebra.Solver.IdempotentCommutativeMonoid

-- An example of how Algebra.IdempotentCommutativeMonoidSolver can be
-- used
import Algebra.Solver.IdempotentCommutativeMonoid.Example

-- Solver for equations in idempotent commutative monoids
import Algebra.Solver.IdempotentCommutativeMonoid.Normal

-- A solver for equations over monoids
import Algebra.Solver.Monoid

-- A solver for equations over monoids
import Algebra.Solver.Monoid.Expression

-- A solver for equations over monoids
import Algebra.Solver.Monoid.Normal

-- A solver for equations over monoids
import Algebra.Solver.Monoid.Solver

-- Old solver for commutative ring or semiring equalities
import Algebra.Solver.Ring

-- Commutative semirings with some additional structure ("almost"
-- commutative rings), used by the ring solver
import Algebra.Solver.Ring.AlmostCommutativeRing

-- Some boring lemmas used by the ring solver
import Algebra.Solver.Ring.Lemmas

-- Instantiates the ring solver, using the natural numbers as the
-- coefficient "ring"
import Algebra.Solver.Ring.NaturalCoefficients

-- Instantiates the natural coefficients ring solver, using coefficient
-- equality induced by ℕ.
import Algebra.Solver.Ring.NaturalCoefficients.Default

-- Instantiates the ring solver with two copies of the same ring with
-- decidable equality
import Algebra.Solver.Ring.Simple

-- Some algebraic structures (not packed up with sets, operations, etc.)
import Algebra.Structures

-- Ways to give instances of certain structures where some fields can
-- be given in terms of others. Re-exported via `Algebra`.
import Algebra.Structures.Biased

-- Results concerning double negation elimination.
import Axiom.DoubleNegationElimination

-- Results concerning the excluded middle axiom.
import Axiom.ExcludedMiddle

-- Results concerning function extensionality for propositional equality
import Axiom.Extensionality.Heterogeneous

-- Results concerning function extensionality for propositional equality
import Axiom.Extensionality.Propositional

-- Results concerning uniqueness of identity proofs
import Axiom.UniquenessOfIdentityProofs

-- Results concerning uniqueness of identity proofs, with axiom K
import Axiom.UniquenessOfIdentityProofs.WithK

-- M-types (the dual of W-types)
import Codata.Guarded.M

-- Infinite streams defined as coinductive records
import Codata.Guarded.Stream

-- Properties of infinite streams defined as coinductive records
import Codata.Guarded.Stream.Properties

-- Coinductive pointwise lifting of relations to streams
import Codata.Guarded.Stream.Relation.Binary.Pointwise

-- Streams where all elements satisfy a given property
import Codata.Guarded.Stream.Relation.Unary.All

-- Streams where at least one element satisfies a given property
import Codata.Guarded.Stream.Relation.Unary.Any

-- "Finite" sets indexed on coinductive "natural" numbers
import Codata.Musical.Cofin

-- Coinductive "natural" numbers
import Codata.Musical.Conat

-- Coinductive "natural" numbers: base type and operations
import Codata.Musical.Conat.Base

-- M-types (the dual of W-types)
import Codata.Musical.M

-- Indexed M-types (the dual of indexed W-types aka Petersson-Synek
-- trees).
import Codata.Musical.M.Indexed

-- Basic types related to coinduction
import Codata.Musical.Notation

-- Booleans
import Data.Bool

-- The type for booleans and some operations
import Data.Bool.Base

-- Instances for booleans
import Data.Bool.Instances

-- A bunch of properties
import Data.Bool.Properties

-- Showing booleans
import Data.Bool.Show

-- Automatic solvers for equations over booleans
import Data.Bool.Solver

-- Characters
import Data.Char

-- Basic definitions for Characters
import Data.Char.Base

-- Instances for characters
import Data.Char.Instances

-- Properties of operations on characters
import Data.Char.Properties

-- Containers, based on the work of Abbott and others
import Data.Container

-- Container combinators
import Data.Container.Combinator

-- Correctness proofs for container combinators
import Data.Container.Combinator.Properties

-- Fixpoints for containers - using guardedness
import Data.Container.Fixpoints.Guarded

-- The free monad construction on containers
import Data.Container.FreeMonad

-- Indexed containers aka interaction structures aka polynomial
-- functors. The notation and presentation here is closest to that of
-- Hancock and Hyvernat in "Programming interfaces and basic topology"
-- (2006/9).
import Data.Container.Indexed

-- Indexed container combinators
import Data.Container.Indexed.Combinator

-- Greatest fixpoint for indexed containers - using guardedness
import Data.Container.Indexed.Fixpoints.Guarded

-- The free monad construction on indexed containers
import Data.Container.Indexed.FreeMonad

-- Equality over indexed container extensions parametrised by a setoid
import Data.Container.Indexed.Relation.Binary.Equality.Setoid

-- Pointwise equality for indexed containers
import Data.Container.Indexed.Relation.Binary.Pointwise

-- Properties of pointwise equality for indexed containers
import Data.Container.Indexed.Relation.Binary.Pointwise.Properties

-- Some code related to indexed containers that uses heterogeneous
-- equality
import Data.Container.Indexed.WithK

-- Membership for containers
import Data.Container.Membership

-- Container Morphisms
import Data.Container.Morphism

-- Propertiers of any for containers
import Data.Container.Morphism.Properties

-- Properties of operations on containers
import Data.Container.Properties

-- Several kinds of "relatedness" for containers such as equivalences,
-- surjections and bijections
import Data.Container.Related

-- Equality over container extensions parametrised by some setoid
import Data.Container.Relation.Binary.Equality.Setoid

-- Pointwise equality for containers
import Data.Container.Relation.Binary.Pointwise

-- Properties of pointwise equality for containers
import Data.Container.Relation.Binary.Pointwise.Properties

-- All (□) for containers
import Data.Container.Relation.Unary.All

-- Any (◇) for containers
import Data.Container.Relation.Unary.Any

-- Propertiers of any for containers
import Data.Container.Relation.Unary.Any.Properties

-- A way to specify that a function's argument takes a default value
-- if the argument is not passed explicitly.
import Data.Default

-- Lists with fast append
import Data.DifferenceList

-- Natural numbers with fast addition (for use together with
-- DifferenceVec)
import Data.DifferenceNat

-- Vectors with fast append
import Data.DifferenceVec

-- Digits and digit expansions
import Data.Digit

-- Properties of digits and digit expansions
import Data.Digit.Properties

-- Empty type, judgementally proof irrelevant, Level-monomorphic
import Data.Empty

-- An irrelevant version of ⊥-elim
import Data.Empty.Irrelevant

-- Level polymorphic Empty type
import Data.Empty.Polymorphic

-- Finite sets
import Data.Fin

-- Finite sets
import Data.Fin.Base

-- Induction over Fin
import Data.Fin.Induction

-- Instances for finite sets
import Data.Fin.Instances

-- Fin Literals
import Data.Fin.Literals

-- Patterns for Fin
import Data.Fin.Patterns

-- Bijections on finite sets (i.e. permutations).
import Data.Fin.Permutation

-- Component functions of permutations found in `Data.Fin.Permutation`
import Data.Fin.Permutation.Components

-- Decomposition of permutations into a list of transpositions.
import Data.Fin.Permutation.Transposition.List

-- Properties related to Fin, and operations making use of these
-- properties (or other properties not available in Data.Fin)
import Data.Fin.Properties

-- Reflection utilities for Fin
import Data.Fin.Reflection

-- The 'top' view of Fin.
import Data.Fin.Relation.Unary.Top

-- Showing finite numbers
import Data.Fin.Show

-- Subsets of finite sets
import Data.Fin.Subset

-- Induction over Subset
import Data.Fin.Subset.Induction

-- Some properties about subsets
import Data.Fin.Subset.Properties

-- Substitutions
import Data.Fin.Substitution

-- Substitution lemmas
import Data.Fin.Substitution.Lemmas

-- Application of substitutions to lists, along with various lemmas
import Data.Fin.Substitution.List

-- Floating point numbers
import Data.Float

-- Floats: basic types and operations
import Data.Float.Base

-- Instances for floating point numbers
import Data.Float.Instances

-- Properties of operations on floats
import Data.Float.Properties

-- Directed acyclic multigraphs
import Data.Graph.Acyclic

-- Integers
import Data.Integer

-- Integers, basic types and operations
import Data.Integer.Base

-- Coprimality
import Data.Integer.Coprimality

-- Integer division
import Data.Integer.DivMod

-- Unsigned divisibility
import Data.Integer.Divisibility

-- Alternative definition of divisibility without using modulus.
import Data.Integer.Divisibility.Signed

-- Greatest Common Divisor for integers
import Data.Integer.GCD

-- Instances for integers
import Data.Integer.Instances

-- Least Common Multiple for integers
import Data.Integer.LCM

-- Integer Literals
import Data.Integer.Literals

-- Some properties about integers
import Data.Integer.Properties

-- Some extra lemmas about natural numbers only needed for
-- Data.Integer.Properties (for distributivity)
import Data.Integer.Properties.NatLemmas

-- Showing integers
import Data.Integer.Show

-- Automatic solvers for equations over integers
import Data.Integer.Solver

-- Automatic solvers for equations over integers
import Data.Integer.Tactic.RingSolver

-- Wrapper for the proof irrelevance modality
import Data.Irrelevant

-- Lists
import Data.List

-- Lists, basic types and operations
import Data.List.Base

-- A data structure which keeps track of an upper bound on the number
-- of elements /not/ in a given list
import Data.List.Countdown

-- An effectful view of List
import Data.List.Effectful

-- List is Foldable
import Data.List.Effectful.Foldable

-- An effectful view of List
import Data.List.Effectful.Transformer

-- Finding the maximum/minimum values in a list
import Data.List.Extrema

-- Finding the maximum/minimum values in a list, specialised for Nat
import Data.List.Extrema.Nat

-- Fresh lists, a proof relevant variant of Catarina Coquand's contexts
-- in "A Formalised Proof of the Soundness and Completeness of a Simply
-- Typed Lambda-Calculus with Explicit Substitutions"
import Data.List.Fresh

-- Membership predicate for fresh lists
import Data.List.Fresh.Membership.Setoid

-- Properties of the membership predicate for fresh lists
import Data.List.Fresh.Membership.Setoid.Properties

-- A non-empty fresh list
import Data.List.Fresh.NonEmpty

-- Properties of fresh lists and functions acting on them
import Data.List.Fresh.Properties

-- All predicate transformer for fresh lists
import Data.List.Fresh.Relation.Unary.All

-- Properties of All predicate transformer for fresh lists
import Data.List.Fresh.Relation.Unary.All.Properties

-- Any predicate transformer for fresh lists
import Data.List.Fresh.Relation.Unary.Any

-- Properties of Any predicate transformer for fresh lists
import Data.List.Fresh.Relation.Unary.Any.Properties

-- Typeclass instances for List
import Data.List.Instances

-- An alternative definition of mutually-defined lists and non-empty
-- lists, using the Kleene star and plus.
import Data.List.Kleene

-- A different interface to the Kleene lists, designed to mimic
-- Data.List.
import Data.List.Kleene.AsList

-- Lists, based on the Kleene star and plus, basic types and operations.
import Data.List.Kleene.Base

-- List Literals
import Data.List.Literals

-- Decidable propositional membership over lists
import Data.List.Membership.DecPropositional

-- Decidable setoid membership over lists
import Data.List.Membership.DecSetoid

-- Data.List.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
import Data.List.Membership.Propositional

-- Properties related to propositional list membership
import Data.List.Membership.Propositional.Properties

-- Properties related to propositional list membership, that rely on
-- the K rule
import Data.List.Membership.Propositional.Properties.WithK

-- List membership and some related definitions
import Data.List.Membership.Setoid

-- Properties related to setoid list membership
import Data.List.Membership.Setoid.Properties

-- Nondependent N-ary functions manipulating lists
import Data.List.Nary.NonDependent

-- Non-empty lists
import Data.List.NonEmpty

-- Non-empty lists: base type and operations
import Data.List.NonEmpty.Base

-- An effectful view of List⁺
import Data.List.NonEmpty.Effectful

-- An effectful view of List
import Data.List.NonEmpty.Effectful.Transformer

-- Typeclass instances for List⁺
import Data.List.NonEmpty.Instances

-- Properties of non-empty lists
import Data.List.NonEmpty.Properties

-- Non-empty lists where all elements satisfy a given property
import Data.List.NonEmpty.Relation.Unary.All

-- List-related properties
import Data.List.Properties

-- Reflection utilities for List
import Data.List.Reflection

-- Bag and set equality
import Data.List.Relation.Binary.BagAndSetEquality

-- Decidability of the disjoint relation over propositional equality.
import Data.List.Relation.Binary.Disjoint.DecPropositional

-- Decidability of the disjoint relation over setoid equality.
import Data.List.Relation.Binary.Disjoint.DecSetoid

-- Pairs of lists that share no common elements (propositional equality)
import Data.List.Relation.Binary.Disjoint.Propositional

-- Properties of disjoint lists (propositional equality)
import Data.List.Relation.Binary.Disjoint.Propositional.Properties

-- Pairs of lists that share no common elements (setoid equality)
import Data.List.Relation.Binary.Disjoint.Setoid

-- Properties of disjoint lists (setoid equality)
import Data.List.Relation.Binary.Disjoint.Setoid.Properties

-- Decidable pointwise equality over lists using propositional equality
import Data.List.Relation.Binary.Equality.DecPropositional

-- Pointwise decidable equality over lists parameterised by a setoid
import Data.List.Relation.Binary.Equality.DecSetoid

-- Pointwise equality over lists using propositional equality
import Data.List.Relation.Binary.Equality.Propositional

-- Pointwise equality over lists parameterised by a setoid
import Data.List.Relation.Binary.Equality.Setoid

-- Properties of List modulo ≋
import Data.List.Relation.Binary.Equality.Setoid.Properties

-- An inductive definition of the heterogeneous infix relation
import Data.List.Relation.Binary.Infix.Heterogeneous

-- Properties of the heterogeneous infix relation
import Data.List.Relation.Binary.Infix.Heterogeneous.Properties

-- Properties of the homogeneous infix relation
import Data.List.Relation.Binary.Infix.Homogeneous.Properties

-- Lexicographic ordering of lists
import Data.List.Relation.Binary.Lex

-- Lexicographic ordering of lists
import Data.List.Relation.Binary.Lex.NonStrict

-- Lexicographic ordering of lists
import Data.List.Relation.Binary.Lex.Strict

-- A definition for the permutation relation using setoid equality
import Data.List.Relation.Binary.Permutation.Homogeneous

-- An inductive definition for the permutation relation
import Data.List.Relation.Binary.Permutation.Propositional

-- Properties of permutation
import Data.List.Relation.Binary.Permutation.Propositional.Properties

-- Properties of permutation (with K)
import Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK

-- A definition for the permutation relation using setoid equality
import Data.List.Relation.Binary.Permutation.Setoid

-- Properties of permutations using setoid equality
import Data.List.Relation.Binary.Permutation.Setoid.Properties

-- Properties of permutations using setoid equality (on Maybe elements)
import Data.List.Relation.Binary.Permutation.Setoid.Properties.Maybe

-- Pointwise lifting of relations to lists
import Data.List.Relation.Binary.Pointwise

-- Pointwise lifting of relations to lists
import Data.List.Relation.Binary.Pointwise.Base

-- Properties of pointwise lifting of relations to lists
import Data.List.Relation.Binary.Pointwise.Properties

-- An inductive definition of the heterogeneous prefix relation
import Data.List.Relation.Binary.Prefix.Heterogeneous

-- Properties of the heterogeneous prefix relation
import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties

-- Properties of the homogeneous prefix relation
import Data.List.Relation.Binary.Prefix.Homogeneous.Properties

-- An inductive definition of the sublist relation for types which have
-- a decidable equality. This is commonly known as Order Preserving
-- Embeddings (OPE).
import Data.List.Relation.Binary.Sublist.DecPropositional

-- A solver for proving that one list is a sublist of the other for
-- types which enjoy decidable equalities.
import Data.List.Relation.Binary.Sublist.DecPropositional.Solver

-- An inductive definition of the sublist relation with respect to a
-- setoid which is decidable. This is a generalisation of what is
-- commonly known as Order Preserving Embeddings (OPE).
import Data.List.Relation.Binary.Sublist.DecSetoid

-- A solver for proving that one list is a sublist of the other.
import Data.List.Relation.Binary.Sublist.DecSetoid.Solver

-- An inductive definition of the heterogeneous sublist relation
-- This is a generalisation of what is commonly known as Order
-- Preserving Embeddings (OPE).
import Data.List.Relation.Binary.Sublist.Heterogeneous

-- Properties of the heterogeneous sublist relation
import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties

-- A solver for proving that one list is a sublist of the other.
import Data.List.Relation.Binary.Sublist.Heterogeneous.Solver

-- An inductive definition of the sublist relation. This is commonly
-- known as Order Preserving Embeddings (OPE).
import Data.List.Relation.Binary.Sublist.Propositional

-- A larger example for sublists (propositional case):
-- Simply-typed lambda terms with globally unique variables
-- (both bound and free ones).
import Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables

-- Sublist-related properties
import Data.List.Relation.Binary.Sublist.Propositional.Properties

-- Slices in the propositional sublist category.
import Data.List.Relation.Binary.Sublist.Propositional.Slice

-- An inductive definition of the sublist relation with respect to a
-- setoid. This is a generalisation of what is commonly known as Order
-- Preserving Embeddings (OPE).
import Data.List.Relation.Binary.Sublist.Setoid

-- Properties of the setoid sublist relation
import Data.List.Relation.Binary.Sublist.Setoid.Properties

-- Decidability of the subset relation over propositional equality.
import Data.List.Relation.Binary.Subset.DecPropositional

-- Decidability of the subset relation over setoid equality.
import Data.List.Relation.Binary.Subset.DecSetoid

-- The sublist relation over propositional equality.
import Data.List.Relation.Binary.Subset.Propositional

-- Properties of the sublist relation over setoid equality.
import Data.List.Relation.Binary.Subset.Propositional.Properties

-- The extensional sublist relation over setoid equality.
import Data.List.Relation.Binary.Subset.Setoid

-- Properties of the extensional sublist relation over setoid equality.
import Data.List.Relation.Binary.Subset.Setoid.Properties

-- An inductive definition of the heterogeneous suffix relation
import Data.List.Relation.Binary.Suffix.Heterogeneous

-- Properties of the heterogeneous suffix relation
import Data.List.Relation.Binary.Suffix.Heterogeneous.Properties

-- Properties of the homogeneous suffix relation
import Data.List.Relation.Binary.Suffix.Homogeneous.Properties

-- Generalised view of appending two lists into one.
import Data.List.Relation.Ternary.Appending

-- Properties of the generalised view of appending two lists
import Data.List.Relation.Ternary.Appending.Properties

-- Appending of lists using propositional equality
import Data.List.Relation.Ternary.Appending.Propositional

-- Properties of list appending
import Data.List.Relation.Ternary.Appending.Propositional.Properties

-- Appending of lists using setoid equality
import Data.List.Relation.Ternary.Appending.Setoid

-- Properties of list appending
import Data.List.Relation.Ternary.Appending.Setoid.Properties

-- Generalised notion of interleaving two lists into one in an
-- order-preserving manner
import Data.List.Relation.Ternary.Interleaving

-- Properties of general interleavings
import Data.List.Relation.Ternary.Interleaving.Properties

-- Interleavings of lists using propositional equality
import Data.List.Relation.Ternary.Interleaving.Propositional

-- Properties of interleaving using propositional equality
import Data.List.Relation.Ternary.Interleaving.Propositional.Properties

-- Interleavings of lists using setoid equality
import Data.List.Relation.Ternary.Interleaving.Setoid

-- Properties of interleaving using setoid equality
import Data.List.Relation.Ternary.Interleaving.Setoid.Properties

-- Lists where all elements satisfy a given property
import Data.List.Relation.Unary.All

-- Properties related to All
import Data.List.Relation.Unary.All.Properties

-- Lists where every pair of elements are related (symmetrically)
import Data.List.Relation.Unary.AllPairs

-- Properties related to AllPairs
import Data.List.Relation.Unary.AllPairs.Properties

-- Lists where at least one element satisfies a given property
import Data.List.Relation.Unary.Any

-- Properties related to Any
import Data.List.Relation.Unary.Any.Properties

-- Lists which contain every element of a given type
import Data.List.Relation.Unary.Enumerates.Setoid

-- Properties of lists which contain every element of a given type
import Data.List.Relation.Unary.Enumerates.Setoid.Properties

-- First generalizes the idea that an element is the first in a list to
-- satisfy a predicate.
import Data.List.Relation.Unary.First

-- Properties of First
import Data.List.Relation.Unary.First.Properties

-- Property that elements are grouped
import Data.List.Relation.Unary.Grouped

-- Property related to Grouped
import Data.List.Relation.Unary.Grouped.Properties

-- Lists where every consecutative pair of elements is related.
import Data.List.Relation.Unary.Linked

-- Properties related to Linked
import Data.List.Relation.Unary.Linked.Properties

-- Sorted lists
import Data.List.Relation.Unary.Sorted.TotalOrder

-- Sorted lists
import Data.List.Relation.Unary.Sorted.TotalOrder.Properties

-- 'Sufficient' lists: a structurally inductive view of lists xs
-- as given by xs ≡ non-empty prefix + sufficient suffix
import Data.List.Relation.Unary.Sufficient

-- Lists made up entirely of unique elements (setoid equality)
import Data.List.Relation.Unary.Unique.DecPropositional

-- Properties of lists made up entirely of decidably unique elements
import Data.List.Relation.Unary.Unique.DecPropositional.Properties

-- Lists made up entirely of unique elements (setoid equality)
import Data.List.Relation.Unary.Unique.DecSetoid

-- Properties of lists made up entirely of decidably unique elements
import Data.List.Relation.Unary.Unique.DecSetoid.Properties

-- Lists made up entirely of unique elements (propositional equality)
import Data.List.Relation.Unary.Unique.Propositional

-- Properties of unique lists (setoid equality)
import Data.List.Relation.Unary.Unique.Propositional.Properties

-- Lists made up entirely of unique elements (setoid equality)
import Data.List.Relation.Unary.Unique.Setoid

-- Properties of unique lists (setoid equality)
import Data.List.Relation.Unary.Unique.Setoid.Properties

-- Reverse view
import Data.List.Reverse

-- List scans: definitions
import Data.List.Scans.Base

-- List scans: properties
import Data.List.Scans.Properties

-- Showing lists
import Data.List.Show

-- Functions and definitions for sorting lists
import Data.List.Sort

-- The core definition of a sorting algorithm
import Data.List.Sort.Base

-- An implementation of merge sort along with proofs of correctness.
import Data.List.Sort.MergeSort

-- List Zippers, basic types and operations
import Data.List.Zipper

-- List Zipper-related properties
import Data.List.Zipper.Properties

-- The Maybe type
import Data.Maybe

-- The Maybe type and some operations
import Data.Maybe.Base

-- An effectful view of Maybe
import Data.Maybe.Effectful

-- An effectful view of Maybe
import Data.Maybe.Effectful.Transformer

-- Typeclass instances for Maybe
import Data.Maybe.Instances

-- Maybe-related properties
import Data.Maybe.Properties

-- Lifting a relation such that `nothing` is also related to `just`
import Data.Maybe.Relation.Binary.Connected

-- Pointwise lifting of relations to maybes
import Data.Maybe.Relation.Binary.Pointwise

-- Maybes where all the elements satisfy a given property
import Data.Maybe.Relation.Unary.All

-- Properties related to All
import Data.Maybe.Relation.Unary.All.Properties

-- Maybes where one of the elements satisfies a given property
import Data.Maybe.Relation.Unary.Any

-- Natural numbers
import Data.Nat

-- Natural numbers, basic types and operations
import Data.Nat.Base

-- Natural numbers represented in binary natively in Agda.
import Data.Nat.Binary

-- Natural numbers represented in binary.
import Data.Nat.Binary.Base

-- Induction over _<_ for ℕᵇ.
import Data.Nat.Binary.Induction

-- Instances for binary natural numbers
import Data.Nat.Binary.Instances

-- Basic properties of ℕᵇ
import Data.Nat.Binary.Properties

-- Subtraction on Bin and some of its properties.
import Data.Nat.Binary.Subtraction

-- Combinatorial operations
import Data.Nat.Combinatorics

-- Combinatorics operations
import Data.Nat.Combinatorics.Base

-- The specification for combinatorics operations
import Data.Nat.Combinatorics.Specification

-- Coprimality
import Data.Nat.Coprimality

-- Natural number division
import Data.Nat.DivMod

-- More efficient mod and divMod operations (require the K axiom)
import Data.Nat.DivMod.WithK

-- Divisibility
import Data.Nat.Divisibility

-- Greatest common divisor
import Data.Nat.GCD

-- Boring lemmas used in Data.Nat.GCD and Data.Nat.Coprimality
import Data.Nat.GCD.Lemmas

-- A generalisation of the arithmetic operations
import Data.Nat.GeneralisedArithmetic

-- Various forms of induction for natural numbers
import Data.Nat.Induction

-- Definition of and lemmas related to "true infinitely often"
import Data.Nat.InfinitelyOften

-- Instances for natural numbers
import Data.Nat.Instances

-- Least common multiple
import Data.Nat.LCM

-- Natural Literals
import Data.Nat.Literals

-- Logarithm base 2 and respective properties
import Data.Nat.Logarithm

-- Primality
import Data.Nat.Primality

-- Prime factorisation of natural numbers and its properties
import Data.Nat.Primality.Factorisation

-- A bunch of properties about natural number operations
import Data.Nat.Properties

-- Linear congruential pseudo random generators for natural numbers
-- /!\ NB: LCGs must not be used for cryptographic applications
import Data.Nat.PseudoRandom.LCG

-- Reflection utilities for ℕ
import Data.Nat.Reflection

-- Showing natural numbers
import Data.Nat.Show

-- Properties of showing natural numbers
import Data.Nat.Show.Properties

-- Automatic solvers for equations over naturals
import Data.Nat.Solver

-- Automatic solvers for equations over naturals
import Data.Nat.Tactic.RingSolver

-- Natural number types and operations requiring the axiom K.
import Data.Nat.WithK

-- Parity
import Data.Parity

-- Parity
import Data.Parity.Base

-- Instances for parities
import Data.Parity.Instances

-- Some properties about parities
import Data.Parity.Properties

-- Products
import Data.Product

-- Algebraic properties of products
import Data.Product.Algebra

-- Products
import Data.Product.Base

-- Universe-sensitive functor and monad instances for the Product type.
import Data.Product.Effectful.Examples

-- Left-biased universe-sensitive functor and monad instances for the
-- Product type.
import Data.Product.Effectful.Left

-- Base definitions for the left-biased universe-sensitive functor and
-- monad instances for the Product type.
import Data.Product.Effectful.Left.Base

-- Right-biased universe-sensitive functor and monad instances for the
-- Product type.
import Data.Product.Effectful.Right

-- Base definitions for the right-biased universe-sensitive functor
-- and monad instances for the Product type.
import Data.Product.Effectful.Right.Base

-- Dependent product combinators for propositional equality
-- preserving functions
import Data.Product.Function.Dependent.Propositional

-- Dependent product combinators for propositional equality
-- preserving functions
import Data.Product.Function.Dependent.Propositional.WithK

-- Dependent product combinators for setoid equality preserving
-- functions.
import Data.Product.Function.Dependent.Setoid

-- Non-dependent product combinators for propositional equality
-- preserving functions
import Data.Product.Function.NonDependent.Propositional

-- Non-dependent product combinators for setoid equality preserving
-- functions
import Data.Product.Function.NonDependent.Setoid

-- Typeclass instances for products
import Data.Product.Instances

-- Nondependent heterogeneous N-ary products
import Data.Product.Nary.NonDependent

-- Properties of products
import Data.Product.Properties

-- Properties of 'very dependent' map / zipWith over products
import Data.Product.Properties.Dependent

-- Properties, related to products, that rely on the K rule
import Data.Product.Properties.WithK

-- Lexicographic products of binary relations
import Data.Product.Relation.Binary.Lex.NonStrict

-- Lexicographic products of binary relations
import Data.Product.Relation.Binary.Lex.Strict

-- Pointwise lifting of binary relations to sigma types
import Data.Product.Relation.Binary.Pointwise.Dependent

-- Properties that are related to pointwise lifting of binary
-- relations to sigma types and make use of heterogeneous equality
import Data.Product.Relation.Binary.Pointwise.Dependent.WithK

-- Pointwise products of binary relations
import Data.Product.Relation.Binary.Pointwise.NonDependent

-- Lifting of two predicates
import Data.Product.Relation.Unary.All

-- Rational numbers
import Data.Rational

-- Rational numbers
import Data.Rational.Base

-- Instances for rational numbers
import Data.Rational.Instances

-- Rational Literals
import Data.Rational.Literals

-- Properties of Rational numbers
import Data.Rational.Properties

-- Showing rational numbers
import Data.Rational.Show

-- Automatic solvers for equations over rationals
import Data.Rational.Solver

-- Rational numbers in non-reduced form.
import Data.Rational.Unnormalised

-- Rational numbers in non-reduced form.
import Data.Rational.Unnormalised.Base

-- Properties of unnormalized Rational numbers
import Data.Rational.Unnormalised.Properties

-- Showing unnormalised rational numbers
import Data.Rational.Unnormalised.Show

-- Automatic solvers for equations over rationals
import Data.Rational.Unnormalised.Solver

-- Record types with manifest fields and "with", based on Randy
-- Pollack's "Dependently Typed Records in Type Theory"
import Data.Record

-- Refinement type: a value together with a proof irrelevant witness.
import Data.Refinement

-- Refinement type: a value together with a proof irrelevant witness.
import Data.Refinement.Base

-- Properties of refinement types
import Data.Refinement.Properties

-- Predicate lifting for refinement types
import Data.Refinement.Relation.Unary.All

-- Signs
import Data.Sign

-- Signs
import Data.Sign.Base

-- Instances for signs
import Data.Sign.Instances

-- Some properties about signs
import Data.Sign.Properties

-- Bounded vectors (inefficient implementation)
import Data.Star.BoundedVec

-- Decorated star-lists
import Data.Star.Decoration

-- Environments (heterogeneous collections)
import Data.Star.Environment

-- Finite sets defined using the reflexive-transitive closure, Star
import Data.Star.Fin

-- Lists defined in terms of the reflexive-transitive closure, Star
import Data.Star.List

-- Natural numbers defined using the reflexive-transitive closure, Star
import Data.Star.Nat

-- Pointers into star-lists
import Data.Star.Pointer

-- Vectors defined in terms of the reflexive-transitive closure, Star
import Data.Star.Vec

-- Strings
import Data.String

-- Strings: builtin type and basic operations
import Data.String.Base

-- Instances for strings
import Data.String.Instances

-- String Literals
import Data.String.Literals

-- Properties of operations on strings
import Data.String.Properties

-- Sums (disjoint unions)
import Data.Sum

-- Algebraic properties of sums (disjoint unions)
import Data.Sum.Algebra

-- Sums (disjoint unions)
import Data.Sum.Base

-- Usage examples of the effectful view of the Sum type
import Data.Sum.Effectful.Examples

-- An effectful view of the Sum type (Left-biased)
import Data.Sum.Effectful.Left

-- An effectful view of the Sum type (Left-biased)
import Data.Sum.Effectful.Left.Transformer

-- An effectful view of the Sum type (Right-biased)
import Data.Sum.Effectful.Right

-- An effectful view of the Sum type (Right-biased)
import Data.Sum.Effectful.Right.Transformer

-- Sum combinators for propositional equality preserving functions
import Data.Sum.Function.Propositional

-- Sum combinators for setoid equality preserving functions
import Data.Sum.Function.Setoid

-- Typeclass instances for sums
import Data.Sum.Instances

-- Properties of sums (disjoint unions)
import Data.Sum.Properties

-- Sums of binary relations
import Data.Sum.Relation.Binary.LeftOrder

-- Pointwise sum
import Data.Sum.Relation.Binary.Pointwise

-- Heterogeneous `All` predicate for disjoint sums
import Data.Sum.Relation.Unary.All

-- An either-or-both data type
import Data.These

-- An either-or-both data type, basic type and operations
import Data.These.Base

-- Left-biased universe-sensitive functor and monad instances for These.
import Data.These.Effectful.Left

-- Base definitions for the left-biased universe-sensitive functor and
-- monad instances for These.
import Data.These.Effectful.Left.Base

-- Right-biased universe-sensitive functor and monad instances for These.
import Data.These.Effectful.Right

-- Base definitions for the right-biased universe-sensitive functor and
-- monad instances for These.
import Data.These.Effectful.Right.Base

-- Typeclass instances for These
import Data.These.Instances

-- Properties of These
import Data.These.Properties

-- AVL trees
import Data.Tree.AVL

-- Types and functions which are used to keep track of height
-- invariants in AVL Trees
import Data.Tree.AVL.Height

-- AVL trees where the stored values may depend on their key
import Data.Tree.AVL.Indexed

-- AVL trees whose elements satisfy a given property
import Data.Tree.AVL.Indexed.Relation.Unary.All

-- AVL trees where at least one element satisfies a given property
import Data.Tree.AVL.Indexed.Relation.Unary.Any

-- Properties related to Any
import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties

-- Some code related to indexed AVL trees that relies on the K rule
import Data.Tree.AVL.Indexed.WithK

-- Finite maps with indexed keys and values, based on AVL trees
import Data.Tree.AVL.IndexedMap

-- Keys for AVL trees -- the original key type extended with a new
-- minimum and maximum.
import Data.Tree.AVL.Key

-- Maps from keys to values, based on AVL trees
-- This modules provides a simpler map interface, without a dependency
-- between the key and value types.
import Data.Tree.AVL.Map

-- Membership relation for AVL Maps identifying values up to
-- propositional equality.
import Data.Tree.AVL.Map.Membership.Propositional

-- Properties of the membership relation for AVL Maps identifying values
-- up to propositional equality.
import Data.Tree.AVL.Map.Membership.Propositional.Properties

-- AVL trees where at least one element satisfies a given property
import Data.Tree.AVL.Map.Relation.Unary.Any

-- Non-empty AVL trees
import Data.Tree.AVL.NonEmpty

-- Non-empty AVL trees, where equality for keys is propositional equality
import Data.Tree.AVL.NonEmpty.Propositional

-- AVL trees where at least one element satisfies a given property
import Data.Tree.AVL.Relation.Unary.Any

-- Finite sets, based on AVL trees
import Data.Tree.AVL.Sets

-- Membership relation for AVL sets
import Data.Tree.AVL.Sets.Membership

-- Properties of membership for AVL sets
import Data.Tree.AVL.Sets.Membership.Properties

-- Values for AVL trees
-- Values must respect the underlying equivalence on keys
import Data.Tree.AVL.Value

-- Binary Trees
import Data.Tree.Binary

-- Properties of binary trees
import Data.Tree.Binary.Properties

-- Pointwise lifting of a predicate to a binary tree
import Data.Tree.Binary.Relation.Unary.All

-- Properties of the pointwise lifting of a predicate to a binary tree
import Data.Tree.Binary.Relation.Unary.All.Properties

-- Zippers for Binary Trees
import Data.Tree.Binary.Zipper

-- Tree Zipper-related properties
import Data.Tree.Binary.Zipper.Properties

-- The unit type, Level-monomorphic version
import Data.Unit

-- The unit type and the total relation on unit
import Data.Unit.Base

-- Instances for the unit type
import Data.Unit.Instances

-- Some unit types
import Data.Unit.NonEta

-- The universe polymorphic unit type and the total relation on unit
import Data.Unit.Polymorphic

-- A universe polymorphic unit type, as a Lift of the Level 0 one.
import Data.Unit.Polymorphic.Base

-- Instances for the polymorphic unit type
import Data.Unit.Polymorphic.Instances

-- Properties of the polymorphic unit type
-- Defines Decidable Equality and Decidable Ordering as well
import Data.Unit.Polymorphic.Properties

-- Properties of the unit type
import Data.Unit.Properties

-- Universes
import Data.Universe

-- Indexed universes
import Data.Universe.Indexed

-- Vectors
import Data.Vec

-- Vectors, basic types and operations
import Data.Vec.Base

-- Bounded vectors
import Data.Vec.Bounded

-- Bounded vectors, basic types and operations
import Data.Vec.Bounded.Base

-- Showing bounded vectors
import Data.Vec.Bounded.Show

-- An effectful view of Vec
import Data.Vec.Effectful

-- Vec is Foldable
import Data.Vec.Effectful.Foldable

-- An effectful view of Vec
import Data.Vec.Effectful.Transformer

-- Vectors defined as functions from a finite set to a type.
import Data.Vec.Functional

-- Some Vector-related properties
import Data.Vec.Functional.Properties

-- Pointwise lifting of relations over Vector
import Data.Vec.Functional.Relation.Binary.Equality.Setoid

-- Permutation relations over Vector
import Data.Vec.Functional.Relation.Binary.Permutation

-- Properties of permutation
import Data.Vec.Functional.Relation.Binary.Permutation.Properties

-- Pointwise lifting of relations over Vector
import Data.Vec.Functional.Relation.Binary.Pointwise

-- Properties related to Pointwise
import Data.Vec.Functional.Relation.Binary.Pointwise.Properties

-- Universal lifting of predicates over Vectors
import Data.Vec.Functional.Relation.Unary.All

-- Properties related to All
import Data.Vec.Functional.Relation.Unary.All.Properties

-- Existential lifting of predicates over Vectors
import Data.Vec.Functional.Relation.Unary.Any

-- Typeclass instances for Vec
import Data.Vec.Instances

-- Decidable propositional membership over vectors
import Data.Vec.Membership.DecPropositional

-- Decidable setoid membership over vectors.
import Data.Vec.Membership.DecSetoid

-- Data.Vec.Any.Membership instantiated with propositional equality,
-- along with some additional definitions.
import Data.Vec.Membership.Propositional

-- Properties of membership of vectors based on propositional equality.
import Data.Vec.Membership.Propositional.Properties

-- Membership of vectors, along with some additional definitions.
import Data.Vec.Membership.Setoid

-- Code for converting Vec A n → B to and from n-ary functions
import Data.Vec.N-ary

-- Some Vec-related properties
import Data.Vec.Properties

-- Some Vec-related properties that depend on the K rule or make use
-- of heterogeneous equality
import Data.Vec.Properties.WithK

-- Vectors defined by recursion
import Data.Vec.Recursive

-- An effectful view of vectors defined by recursion
import Data.Vec.Recursive.Effectful

-- Properties of n-ary products
import Data.Vec.Recursive.Properties

-- Reflection utilities for Vector
import Data.Vec.Reflection

-- An equational reasoning library for propositional equality over
-- vectors of different indices using cast.
import Data.Vec.Relation.Binary.Equality.Cast

-- Decidable vector equality over propositional equality
import Data.Vec.Relation.Binary.Equality.DecPropositional

-- Decidable semi-heterogeneous vector equality over setoids
import Data.Vec.Relation.Binary.Equality.DecSetoid

-- Vector equality over propositional equality
import Data.Vec.Relation.Binary.Equality.Propositional

-- Code related to vector equality over propositional equality that
-- makes use of heterogeneous equality
import Data.Vec.Relation.Binary.Equality.Propositional.WithK

-- Semi-heterogeneous vector equality over setoids
import Data.Vec.Relation.Binary.Equality.Setoid

-- Lexicographic ordering of same-length vector
import Data.Vec.Relation.Binary.Lex.NonStrict

-- Lexicographic ordering of lists of same-length vectors
import Data.Vec.Relation.Binary.Lex.Strict

-- Extensional pointwise lifting of relations to vectors
import Data.Vec.Relation.Binary.Pointwise.Extensional

-- Inductive pointwise lifting of relations to vectors
import Data.Vec.Relation.Binary.Pointwise.Inductive

-- Vectors where all elements satisfy a given property
import Data.Vec.Relation.Unary.All

-- Properties related to All
import Data.Vec.Relation.Unary.All.Properties

-- Vectors where every pair of elements are related (symmetrically)
import Data.Vec.Relation.Unary.AllPairs

-- Properties related to AllPairs
import Data.Vec.Relation.Unary.AllPairs.Properties

-- Vectors where at least one element satisfies a given property
import Data.Vec.Relation.Unary.Any

-- Properties of vector's Any
import Data.Vec.Relation.Unary.Any.Properties

-- Vectors where every consecutative pair of elements is related.
import Data.Vec.Relation.Unary.Linked

-- Properties related to Linked
import Data.Vec.Relation.Unary.Linked.Properties

-- Vectors made up entirely of unique elements (propositional equality)
import Data.Vec.Relation.Unary.Unique.Propositional

-- Properties of unique vectors (setoid equality)
import Data.Vec.Relation.Unary.Unique.Propositional.Properties

-- Vectors made up entirely of unique elements (setoid equality)
import Data.Vec.Relation.Unary.Unique.Setoid

-- Properties of unique vectors (setoid equality)
import Data.Vec.Relation.Unary.Unique.Setoid.Properties

-- Showing vectors
import Data.Vec.Show

-- W-types
import Data.W

-- Indexed W-types aka Petersson-Synek trees
import Data.W.Indexed

-- Some code related to the W type that relies on the K rule
import Data.W.WithK

-- Machine words
import Data.Word64

-- Machine words: basic type and conversion functions
import Data.Word64.Base

-- Instances for words
import Data.Word64.Instances

-- Word64 Literals
import Data.Word64.Literals

-- Properties of operations on machine words
import Data.Word64.Properties

-- Turn a relation into a record definition so as to remember the things
-- being related.
-- This module has a readme file: README.Data.Wrap
import Data.Wrap

-- Applicative functors
import Effect.Applicative

-- Indexed applicative functors
import Effect.Applicative.Indexed

-- Applicative functors on indexed sets (predicates)
import Effect.Applicative.Predicate

-- Type constructors giving rise to a semigroup at every type
-- e.g. (List, _++_)
import Effect.Choice

-- Comonads
import Effect.Comonad

-- Empty values (e.g. [] for List, nothing for Maybe)
import Effect.Empty

-- Foldable functors
import Effect.Foldable

-- Functors
import Effect.Functor

-- Functors on indexed sets (predicates)
import Effect.Functor.Predicate

-- Monads
import Effect.Monad

-- A delimited continuation monad
import Effect.Monad.Continuation

-- The error monad transformer
import Effect.Monad.Error.Transformer

-- An effectful view of the identity function
import Effect.Monad.Identity

-- Typeclass instances for Identity
import Effect.Monad.Identity.Instances

-- Indexed monads
import Effect.Monad.Indexed

-- The partiality monad
import Effect.Monad.Partiality

-- An All predicate for the partiality monad
import Effect.Monad.Partiality.All

-- Typeclass instances for _⊥
import Effect.Monad.Partiality.Instances

-- Monads on indexed sets (predicates)
import Effect.Monad.Predicate

-- The reader monad
import Effect.Monad.Reader

-- The indexed reader monad
import Effect.Monad.Reader.Indexed

-- Instances for the reader monad
import Effect.Monad.Reader.Instances

-- The reader monad transformer
import Effect.Monad.Reader.Transformer

-- Basic type and definition of the reader monad transformer
import Effect.Monad.Reader.Transformer.Base

-- The state monad
import Effect.Monad.State

-- The indexed state monad
import Effect.Monad.State.Indexed

-- Instances for the state monad
import Effect.Monad.State.Instances

-- The state monad transformer
import Effect.Monad.State.Transformer

-- Basic definition and functions on the state monad transformer
import Effect.Monad.State.Transformer.Base

-- The writer monad
import Effect.Monad.Writer

-- The indexed writer monad
import Effect.Monad.Writer.Indexed

-- Instances for the writer monad
import Effect.Monad.Writer.Instances

-- The writer monad transformer
import Effect.Monad.Writer.Transformer

-- Basic type and definition of the writer monad transformer
import Effect.Monad.Writer.Transformer.Base

-- Functions
import Function

-- Simple combinators working solely on and with functions
import Function.Base

-- Bundles for types of functions
import Function.Bundles

-- Relationships between properties of functions. See
-- `Function.Consequences.Propositional` for specialisations to
-- propositional equality.
import Function.Consequences

-- Relationships between properties of functions where the equality
-- over both the domain and codomain is assumed to be _≡_
import Function.Consequences.Propositional

-- Relationships between properties of functions where the equality
-- over both the domain and codomain are assumed to be setoids.
import Function.Consequences.Setoid

-- Composition of functional properties
import Function.Construct.Composition

-- The constant function
import Function.Construct.Constant

-- The identity function
import Function.Construct.Identity

-- Some functional properties are symmetric
import Function.Construct.Symmetry

-- Definitions for types of functions.
import Function.Definitions

-- Bundles for types of functions
import Function.Dependent.Bundles

-- Endomorphisms on a Set
import Function.Endo.Propositional

-- Endomorphisms on a Setoid
import Function.Endo.Setoid

-- An effectful view of the identity function
import Function.Identity.Effectful

-- Operations on Relations for Indexed sets
import Function.Indexed.Bundles

-- Function setoids and related constructions
import Function.Indexed.Relation.Binary.Equality

-- Metrics with arbitrary domains and codomains
import Function.Metric

-- Bundles for metrics
import Function.Metric.Bundles

-- Definitions of properties over distance functions
import Function.Metric.Definitions

-- Metrics with ℕ as the codomain of the metric function
import Function.Metric.Nat

-- Bundles for metrics over ℕ
import Function.Metric.Nat.Bundles

-- Core definitions for metrics over ℕ
import Function.Metric.Nat.Definitions

-- Core definitions for metrics over ℕ
import Function.Metric.Nat.Structures

-- Metrics with ℚ as the codomain of the metric function
import Function.Metric.Rational

-- Bundles for metrics over ℚ
import Function.Metric.Rational.Bundles

-- Core definitions for metrics over ℚ
import Function.Metric.Rational.Definitions

-- Core definitions for metrics over ℚ
import Function.Metric.Rational.Structures

-- Some metric structures (not packed up with sets, operations, etc.)
import Function.Metric.Structures

-- Heterogeneous N-ary Functions
import Function.Nary.NonDependent

-- Heterogeneous N-ary Functions: basic types and operations
import Function.Nary.NonDependent.Base

-- Basic properties of the function type
import Function.Properties

-- Some basic properties of bijections.
import Function.Properties.Bijection

-- Some basic properties of equivalences. This file is designed to be
-- imported qualified.
import Function.Properties.Equivalence

-- Properties for injections
import Function.Properties.Injection

-- Properties of inverses.
import Function.Properties.Inverse

-- Half adjoint equivalences
import Function.Properties.Inverse.HalfAdjointEquivalence

-- Properties of right inverses
import Function.Properties.RightInverse

-- Properties of surjections
import Function.Properties.Surjection

-- A module used for creating function pipelines, see
-- README.Function.Reasoning for examples
import Function.Reasoning

-- Relatedness for the function hierarchy
import Function.Related.Propositional

-- Basic lemmas showing that various types are related (isomorphic or
-- equivalent or…)
import Function.Related.TypeIsomorphisms

-- Automatic solver for equations over product and sum types
import Function.Related.TypeIsomorphisms.Solver

-- Function Equality setoid
import Function.Relation.Binary.Setoid.Equality

-- Strict combinators (i.e. that use call-by-value)
import Function.Strict

-- Structures for types of functions
import Function.Structures

-- Ways to give instances of certain structures where some fields can
-- be given in terms of others.
-- The contents of this file should usually be accessed from `Function`.
import Function.Structures.Biased

-- An abstraction of various forms of recursion/induction
import Induction

-- A standard consequence of accessibility/well-foundedness:
-- the impossibility of 'infinite descent' from any (accessible)
-- element x satisfying P to 'smaller' y also satisfying P
import Induction.InfiniteDescent

-- Lexicographic induction
import Induction.Lexicographic

-- Well-founded induction
import Induction.WellFounded

-- Universe levels
import Level

-- Conversion from naturals to universe levels
import Level.Literals

-- Support for reflection
import Reflection

-- The reflected abstract syntax tree
import Reflection.AST

-- Abstractions used in the reflection machinery
import Reflection.AST.Abstraction

-- Alpha equality over terms
import Reflection.AST.AlphaEquality

-- Arguments used in the reflection machinery
import Reflection.AST.Argument

-- Argument information used in the reflection machinery
import Reflection.AST.Argument.Information

-- Modalities used in the reflection machinery
import Reflection.AST.Argument.Modality

-- Argument quantities used in the reflection machinery
import Reflection.AST.Argument.Quantity

-- Argument relevance used in the reflection machinery
import Reflection.AST.Argument.Relevance

-- Argument visibility used in the reflection machinery
import Reflection.AST.Argument.Visibility

-- Weakening, strengthening and free variable check for reflected terms.
import Reflection.AST.DeBruijn

-- Definitions used in the reflection machinery
import Reflection.AST.Definition

-- Instances for reflected syntax
import Reflection.AST.Instances

-- Literals used in the reflection machinery
import Reflection.AST.Literal

-- Metavariables used in the reflection machinery
import Reflection.AST.Meta

-- Names used in the reflection machinery
import Reflection.AST.Name

-- Patterns used in the reflection machinery
import Reflection.AST.Pattern

-- Converting reflection machinery to strings
import Reflection.AST.Show

-- Terms used in the reflection machinery
import Reflection.AST.Term

-- de Bruijn-aware generic traversal of reflected terms.
import Reflection.AST.Traversal

-- A universe for the types involved in the reflected syntax.
import Reflection.AST.Universe

-- Annotated reflected syntax.
import Reflection.AnnotatedAST

-- Computing free variable annotations on reflected syntax.
import Reflection.AnnotatedAST.Free

-- Support for system calls as part of reflection
import Reflection.External

-- The TC (Type Checking) monad
import Reflection.TCM

-- Typeclass instances for TC
import Reflection.TCM.Effectful

-- Printf-style versions of typeError and debugPrint
import Reflection.TCM.Format

-- Typeclass instances for TC
import Reflection.TCM.Instances

-- Monad syntax for the TC monad
import Reflection.TCM.Syntax

-- Reflection utilities
import Reflection.TCM.Utilities

-- Properties of homogeneous binary relations
import Relation.Binary

-- Bundles for homogeneous binary relations
import Relation.Binary.Bundles

-- Raw bundles for homogeneous binary relations
import Relation.Binary.Bundles.Raw

-- Some properties imply others
import Relation.Binary.Consequences

-- A pointwise lifting of a relation to incorporate new extrema.
import Relation.Binary.Construct.Add.Extrema.Equality

-- The lifting of a non-strict order to incorporate new extrema
import Relation.Binary.Construct.Add.Extrema.NonStrict

-- The lifting of a strict order to incorporate new extrema
import Relation.Binary.Construct.Add.Extrema.Strict

-- A pointwise lifting of a relation to incorporate a new infimum.
import Relation.Binary.Construct.Add.Infimum.Equality

-- The lifting of a non-strict order to incorporate a new infimum
import Relation.Binary.Construct.Add.Infimum.NonStrict

-- The lifting of a non-strict order to incorporate a new infimum
import Relation.Binary.Construct.Add.Infimum.Strict

-- A pointwise lifting of a relation to incorporate an additional point.
import Relation.Binary.Construct.Add.Point.Equality

-- A pointwise lifting of a relation to incorporate a new supremum.
import Relation.Binary.Construct.Add.Supremum.Equality

-- The lifting of a non-strict order to incorporate a new supremum
import Relation.Binary.Construct.Add.Supremum.NonStrict

-- The lifting of a strict order to incorporate a new supremum
import Relation.Binary.Construct.Add.Supremum.Strict

-- The universal binary relation
import Relation.Binary.Construct.Always

-- The reflexive, symmetric and transitive closure of a binary
-- relation (aka the equivalence closure).
import Relation.Binary.Construct.Closure.Equivalence

-- Some properties of equivalence closures.
import Relation.Binary.Construct.Closure.Equivalence.Properties

-- Reflexive closures
import Relation.Binary.Construct.Closure.Reflexive

-- Some properties of reflexive closures
import Relation.Binary.Construct.Closure.Reflexive.Properties

-- Some properties of reflexive closures which rely on the K rule
import Relation.Binary.Construct.Closure.Reflexive.Properties.WithK

-- The reflexive transitive closures of McBride, Norell and Jansson
import Relation.Binary.Construct.Closure.ReflexiveTransitive

-- Some properties of reflexive transitive closures.
import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties

-- Properties, related to reflexive transitive closures, that rely on
-- the K rule
import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties.WithK

-- Symmetric closures of binary relations
import Relation.Binary.Construct.Closure.Symmetric

-- Symmetric transitive closures of binary relations
import Relation.Binary.Construct.Closure.SymmetricTransitive

-- Transitive closures
import Relation.Binary.Construct.Closure.Transitive

-- Some code related to transitive closures that relies on the K rule
import Relation.Binary.Construct.Closure.Transitive.WithK

-- Composition of two binary relations
import Relation.Binary.Construct.Composition

-- The binary relation defined by a constant
import Relation.Binary.Construct.Constant

-- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
-- the module `Relation.Binary.Construct.Flip.Ord` this module does not
-- flip the underlying equality.
import Relation.Binary.Construct.Flip.EqAndOrd

-- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
-- the module `Relation.Binary.Construct.Flip.EqAndOrd` this module
-- flips both the relation and the underlying equality.
import Relation.Binary.Construct.Flip.Ord

-- Every respectful unary relation induces a preorder. No claim is
-- made that this preorder is unique.
import Relation.Binary.Construct.FromPred

-- Every respectful binary relation induces a preorder. No claim is
-- made that this preorder is unique.
import Relation.Binary.Construct.FromRel

-- Symmetric interior of a binary relation
import Relation.Binary.Construct.Interior.Symmetric

-- Intersection of two binary relations
import Relation.Binary.Construct.Intersection

-- Conversion of binary operators to binary relations via the left
-- natural order.
import Relation.Binary.Construct.NaturalOrder.Left

-- Conversion of binary operators to binary relations via the right
-- natural order.
import Relation.Binary.Construct.NaturalOrder.Right

-- The empty binary relation
import Relation.Binary.Construct.Never

-- Conversion of _≤_ to _<_
import Relation.Binary.Construct.NonStrictToStrict

-- Many properties which hold for `_∼_` also hold for `_∼_ on f`
import Relation.Binary.Construct.On

-- Conversion of < to ≤, along with a number of properties
import Relation.Binary.Construct.StrictToNonStrict

-- Substituting equalities for binary relations
import Relation.Binary.Construct.Subst.Equality

-- Union of two binary relations
import Relation.Binary.Construct.Union

-- Properties of binary relations
import Relation.Binary.Definitions

-- Heterogeneous equality
import Relation.Binary.HeterogeneousEquality

-- Quotients for Heterogeneous equality
import Relation.Binary.HeterogeneousEquality.Quotients

-- Example of a Quotient: ℤ as (ℕ × ℕ / ∼)
import Relation.Binary.HeterogeneousEquality.Quotients.Examples

-- Heterogeneously-indexed binary relations
import Relation.Binary.Indexed.Heterogeneous

-- Indexed binary relations
import Relation.Binary.Indexed.Heterogeneous.Bundles

-- Instantiates indexed binary structures at an index to the equivalent
-- non-indexed structures.
import Relation.Binary.Indexed.Heterogeneous.Construct.At

-- Creates trivially indexed records from their non-indexed counterpart.
import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial

-- Indexed binary relations
import Relation.Binary.Indexed.Heterogeneous.Definitions

-- Indexed binary relations
import Relation.Binary.Indexed.Heterogeneous.Structures

-- Homogeneously-indexed binary relations
import Relation.Binary.Indexed.Homogeneous

-- Homogeneously-indexed binary relations
import Relation.Binary.Indexed.Homogeneous.Bundles

-- Instantiating homogeneously indexed bundles at a particular index
import Relation.Binary.Indexed.Homogeneous.Construct.At

-- Homogeneously-indexed binary relations
import Relation.Binary.Indexed.Homogeneous.Definitions

-- Homogeneously-indexed binary relations
import Relation.Binary.Indexed.Homogeneous.Structures

-- Order-theoretic lattices
import Relation.Binary.Lattice

-- Bundles for order-theoretic lattices
import Relation.Binary.Lattice.Bundles

-- Definitions for order-theoretic lattices
import Relation.Binary.Lattice.Definitions

-- Properties satisfied by bounded join semilattices
import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice

-- Properties satisfied by bounded lattice
import Relation.Binary.Lattice.Properties.BoundedLattice

-- Properties satisfied by bounded meet semilattices
import Relation.Binary.Lattice.Properties.BoundedMeetSemilattice

-- Properties for distributive lattice
import Relation.Binary.Lattice.Properties.DistributiveLattice

-- Properties satisfied by Heyting Algebra
import Relation.Binary.Lattice.Properties.HeytingAlgebra

-- Properties satisfied by join semilattices
import Relation.Binary.Lattice.Properties.JoinSemilattice

-- Properties satisfied by lattices
import Relation.Binary.Lattice.Properties.Lattice

-- Properties satisfied by meet semilattices
import Relation.Binary.Lattice.Properties.MeetSemilattice

-- Structures for order-theoretic lattices
import Relation.Binary.Lattice.Structures

-- Order morphisms
import Relation.Binary.Morphism

-- Bundles for morphisms between binary relations
import Relation.Binary.Morphism.Bundles

-- The composition of morphisms between binary relations
import Relation.Binary.Morphism.Construct.Composition

-- Constant morphisms between binary relations
import Relation.Binary.Morphism.Construct.Constant

-- The identity morphism for binary relations
import Relation.Binary.Morphism.Construct.Identity

-- Basic definitions for morphisms between algebraic structures
import Relation.Binary.Morphism.Definitions

-- Consequences of a monomorphism between orders
import Relation.Binary.Morphism.OrderMonomorphism

-- Consequences of a monomorphism between binary relations
import Relation.Binary.Morphism.RelMonomorphism

-- Order morphisms
import Relation.Binary.Morphism.Structures

-- Apartness properties
import Relation.Binary.Properties.ApartnessRelation

-- Every decidable setoid induces tight apartness relation.
import Relation.Binary.Properties.DecSetoid

-- Properties satisfied by decidable total orders
import Relation.Binary.Properties.DecTotalOrder

-- Properties satisfied by posets
import Relation.Binary.Properties.Poset

-- Properties satisfied by preorders
import Relation.Binary.Properties.Preorder

-- Additional properties for setoids
import Relation.Binary.Properties.Setoid

-- Properties satisfied by strict partial orders
import Relation.Binary.Properties.StrictPartialOrder

-- Properties satisfied by strict partial orders
import Relation.Binary.Properties.StrictTotalOrder

-- Properties satisfied by total orders
import Relation.Binary.Properties.TotalOrder

-- Propositional (intensional) equality
import Relation.Binary.PropositionalEquality

-- Propositional (intensional) equality - Algebraic structures
import Relation.Binary.PropositionalEquality.Algebra

-- Propositional equality
import Relation.Binary.PropositionalEquality.Properties

-- Some code related to propositional equality that relies on the K
-- rule
import Relation.Binary.PropositionalEquality.WithK

-- The basic code for equational reasoning with three relations:
-- equality and apartness
import Relation.Binary.Reasoning.Base.Apartness

-- The basic code for equational reasoning with two relations:
-- equality and some other ordering.
import Relation.Binary.Reasoning.Base.Double

-- The basic code for equational reasoning with a non-reflexive relation
import Relation.Binary.Reasoning.Base.Partial

-- The basic code for equational reasoning with a single relation
import Relation.Binary.Reasoning.Base.Single

-- The basic code for equational reasoning with three relations:
-- equality, strict ordering and non-strict ordering.
import Relation.Binary.Reasoning.Base.Triple

-- Convenient syntax for "equational reasoning" in multiple Setoids.
import Relation.Binary.Reasoning.MultiSetoid

-- Convenient syntax for "equational reasoning" using a partial order
import Relation.Binary.Reasoning.PartialOrder

-- Convenient syntax for reasoning with a partial setoid
import Relation.Binary.Reasoning.PartialSetoid

-- Convenient syntax for "equational reasoning" using a preorder
import Relation.Binary.Reasoning.Preorder

-- Convenient syntax for reasoning with a setoid
import Relation.Binary.Reasoning.Setoid

-- Convenient syntax for "equational reasoning" using a strict partial
-- order.
import Relation.Binary.Reasoning.StrictPartialOrder

-- Syntax for the building blocks of equational reasoning modules
import Relation.Binary.Reasoning.Syntax

-- Helpers intended to ease the development of "tactics" which use
-- proof by reflection
import Relation.Binary.Reflection

-- Concepts from rewriting theory
-- Definitions are based on "Term Rewriting Systems" by J.W. Klop
import Relation.Binary.Rewriting

-- Structures for homogeneous binary relations
import Relation.Binary.Structures

-- Ways to give instances of certain structures where some fields can
-- be given in terms of others
import Relation.Binary.Structures.Biased

-- Typeclasses for use with instance arguments
import Relation.Binary.TypeClasses

-- Heterogeneous N-ary Relations
import Relation.Nary

-- Operations on nullary relations (like negation and decidability)
import Relation.Nullary

-- Notation for freely adding extrema to any set
import Relation.Nullary.Construct.Add.Extrema

-- Notation for freely adding an infimum to any set
import Relation.Nullary.Construct.Add.Infimum

-- Notation for adding an additional point to any set
import Relation.Nullary.Construct.Add.Point

-- Notation for freely adding a supremum to any set
import Relation.Nullary.Construct.Add.Supremum

-- Operations on and properties of decidable relations
import Relation.Nullary.Decidable

-- Negation indexed by a Level
import Relation.Nullary.Indexed

-- Properties of indexed negation
import Relation.Nullary.Indexed.Negation

-- Properties related to negation
import Relation.Nullary.Negation

-- Recomputable types and their algebra as Harrop formulas
import Relation.Nullary.Recomputable

-- Properties of the `Reflects` construct
import Relation.Nullary.Reflects

-- A universe of proposition functors, along with some properties
import Relation.Nullary.Universe

-- Unary relations
import Relation.Unary

-- Algebraic properties of constructions over unary relations
import Relation.Unary.Algebra

-- Closures of a unary relation with respect to a binary one.
import Relation.Unary.Closure.Base

-- Closure of a unary relation with respect to a preorder
import Relation.Unary.Closure.Preorder

-- Closures of a unary relation with respect to a strict partial order
import Relation.Unary.Closure.StrictPartialOrder

-- Some properties imply others
import Relation.Unary.Consequences

-- Indexed unary relations
import Relation.Unary.Indexed

-- Polymorphic versions of standard definitions in Relation.Unary
import Relation.Unary.Polymorphic

-- Properties of polymorphic versions of standard definitions in
-- Relation.Unary
import Relation.Unary.Polymorphic.Properties

-- Predicate transformers
import Relation.Unary.PredicateTransformer

-- Properties of constructions over unary relations
import Relation.Unary.Properties

-- Equality of unary relations
import Relation.Unary.Relation.Binary.Equality

-- Order properties of the subset relations _⊆_ and _⊂_
import Relation.Unary.Relation.Binary.Subset

-- ANSI escape codes
import System.Console.ANSI

-- A simple tactic for used to automatically compute the function
-- argument to cong.
import Tactic.Cong

-- Reflection-based solver for monoid equalities
import Tactic.MonoidSolver

-- A solver that uses reflection to automatically obtain and solve
-- equations over rings.
import Tactic.RingSolver

-- Almost commutative rings
import Tactic.RingSolver.Core.AlmostCommutativeRing

-- A type for expressions over a raw ring.
import Tactic.RingSolver.Core.Expression

-- Simple implementation of sets of ℕ.
import Tactic.RingSolver.Core.NatSet

-- Sparse polynomials in a commutative ring, encoded in Horner normal
-- form.
import Tactic.RingSolver.Core.Polynomial.Base

-- Some specialised instances of the ring solver
import Tactic.RingSolver.Core.Polynomial.Homomorphism

-- Homomorphism proofs for addition over polynomials
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition

-- Homomorphism proofs for constants over polynomials
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants

-- Homomorphism proofs for exponentiation over polynomials
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation

-- Lemmas for use in proving the polynomial homomorphism.
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas

-- Homomorphism proofs for multiplication over polynomials
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication

-- Homomorphism proofs for negation over polynomials
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation

-- Homomorphism proofs for variables and constants over polynomials
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables

-- Bundles of parameters for passing to the Ring Solver
import Tactic.RingSolver.Core.Polynomial.Parameters

-- Polynomial reasoning
import Tactic.RingSolver.Core.Polynomial.Reasoning

-- "Evaluating" a polynomial, using Horner's method.
import Tactic.RingSolver.Core.Polynomial.Semantics

-- An implementation of the ring solver that requires you to manually
-- pass the equation you wish to solve.
import Tactic.RingSolver.NonReflective

-- Format strings for Printf and Scanf
import Text.Format

-- Format strings for Printf and Scanf
import Text.Format.Generic

-- Printf
import Text.Printf

-- Generic printf function.
import Text.Printf.Generic

-- Regular expressions
import Text.Regex

-- Regular expressions: basic types and semantics
import Text.Regex.Base

-- Regular expressions: Brzozowski derivative
import Text.Regex.Derivative.Brzozowski

-- Properties of regular expressions and their semantics
import Text.Regex.Properties

-- Regular expressions: search algorithms
import Text.Regex.Search

-- Regular expressions: smart constructors
-- Computing the Brzozowski derivative of a regular expression may lead
-- to a blow-up in the size of the expression. To keep it tractable it
-- is crucial to use smart constructors.
import Text.Regex.SmartConstructors

-- Regular expressions acting on strings
import Text.Regex.String

-- Fancy display functions for List-based tables
import Text.Tabular.Base

-- Fancy display functions for List-based tables
import Text.Tabular.List

-- Fancy display functions for Vec-based tables
import Text.Tabular.Vec