module index where

-- You probably want to start with this module:
import README

-- For a brief presentation of every single module, head over to
import Everything

-- Otherwise, here is an exhaustive, stern list of all the available modules:
import Algebra
import Algebra.CommutativeMonoidSolver
import Algebra.CommutativeMonoidSolver.Example
import Algebra.FunctionProperties
import Algebra.FunctionProperties.Consequences
import Algebra.FunctionProperties.Core
import Algebra.IdempotentCommutativeMonoidSolver
import Algebra.IdempotentCommutativeMonoidSolver.Example
import Algebra.Monoid-solver
import Algebra.Morphism
import Algebra.Operations.CommutativeMonoid
import Algebra.Operations.Semiring
import Algebra.Properties.AbelianGroup
import Algebra.Properties.BooleanAlgebra
import Algebra.Properties.BooleanAlgebra.Expression
import Algebra.Properties.DistributiveLattice
import Algebra.Properties.Group
import Algebra.Properties.Lattice
import Algebra.Properties.Ring
import Algebra.RingSolver
import Algebra.RingSolver.AlmostCommutativeRing
import Algebra.RingSolver.Lemmas
import Algebra.RingSolver.Natural-coefficients
import Algebra.RingSolver.Simple
import Algebra.Structures
import Category.Applicative
import Category.Applicative.Indexed
import Category.Applicative.Predicate
import Category.Functor
import Category.Functor.Identity
import Category.Functor.Predicate
import Category.Monad
import Category.Monad.Continuation
import Category.Monad.Identity
import Category.Monad.Indexed
import Category.Monad.Partiality
import Category.Monad.Partiality.All
import Category.Monad.Predicate
import Category.Monad.State
import Coinduction
import Data.AVL
import Data.AVL.Height
import Data.AVL.Indexed
import Data.AVL.IndexedMap
import Data.AVL.Key
import Data.AVL.Sets
import Data.Bin
import Data.Bin.Properties
import Data.Bool
import Data.Bool.Base
import Data.Bool.Properties
import Data.Bool.Show
import Data.BoundedVec
import Data.BoundedVec.Inefficient
import Data.Char
import Data.Char.Base
import Data.Char.Core
import Data.Cofin
import Data.Colist
import Data.Colist.Infinite-merge
import Data.Conat
import Data.Container
import Data.Container.Any
import Data.Container.Combinator
import Data.Container.FreeMonad
import Data.Container.Indexed
import Data.Container.Indexed.Combinator
import Data.Container.Indexed.Core
import Data.Container.Indexed.FreeMonad
import Data.Covec
import Data.DifferenceList
import Data.DifferenceNat
import Data.DifferenceVec
import Data.Digit
import Data.Empty
import Data.Empty.Irrelevant
import Data.Fin
import Data.Fin.Dec
import Data.Fin.Permutation
import Data.Fin.Permutation.Components
import Data.Fin.Properties
import Data.Fin.Subset
import Data.Fin.Subset.Properties
import Data.Fin.Substitution
import Data.Fin.Substitution.Example
import Data.Fin.Substitution.Lemmas
import Data.Fin.Substitution.List
import Data.Float
import Data.Graph.Acyclic
import Data.Integer
import Data.Integer.Addition.Properties
import Data.Integer.Base
import Data.Integer.Divisibility
import Data.Integer.Multiplication.Properties
import Data.Integer.Properties
import Data.List
import Data.List.All
import Data.List.All.Properties
import Data.List.Any
import Data.List.Any.Properties
import Data.List.Base
import Data.List.Categorical
import Data.List.Countdown
import Data.List.Membership.DecPropositional
import Data.List.Membership.DecSetoid
import Data.List.Membership.Propositional
import Data.List.Membership.Propositional.Properties
import Data.List.Membership.Propositional.Properties.Core
import Data.List.Membership.Setoid
import Data.List.Membership.Setoid.Properties
import Data.List.NonEmpty
import Data.List.NonEmpty.Properties
import Data.List.Properties
import Data.List.Relation.BagAndSetEquality
import Data.List.Relation.Equality.DecPropositional
import Data.List.Relation.Equality.DecSetoid
import Data.List.Relation.Equality.Propositional
import Data.List.Relation.Equality.Setoid
import Data.List.Relation.Lex.Core
import Data.List.Relation.Lex.NonStrict
import Data.List.Relation.Lex.Strict
import Data.List.Relation.Pointwise
import Data.List.Relation.Sublist.Propositional
import Data.List.Relation.Sublist.Propositional.Properties
import Data.List.Relation.Sublist.Setoid
import Data.List.Relation.Sublist.Setoid.Properties
import Data.List.Reverse
import Data.List.Zipper
import Data.List.Zipper.Properties
import Data.M
import Data.Maybe
import Data.Maybe.Base
import Data.M.Indexed
import Data.Nat
import Data.Nat.Base
import Data.Nat.Coprimality
import Data.Nat.Divisibility
import Data.Nat.DivMod
import Data.Nat.GCD
import Data.Nat.GCD.Lemmas
import Data.Nat.GeneralisedArithmetic
import Data.Nat.InfinitelyOften
import Data.Nat.LCM
import Data.Nat.Primality
import Data.Nat.Properties
import Data.Nat.Properties.Simple
import Data.Nat.Show
import Data.Plus
import Data.Product
import Data.Product.N-ary
import Data.Product.N-ary.Properties
import Data.Product.Properties
import Data.Product.Relation.Lex.NonStrict
import Data.Product.Relation.Lex.Strict
import Data.Product.Relation.Pointwise.Dependent
import Data.Product.Relation.Pointwise.NonDependent
import Data.Rational
import Data.Rational.Properties
import Data.ReflexiveClosure
import Data.Sign
import Data.Sign.Properties
import Data.Star
import Data.Star.BoundedVec
import Data.Star.Decoration
import Data.Star.Environment
import Data.Star.Fin
import Data.Star.List
import Data.Star.Nat
import Data.Star.Pointer
import Data.Star.Properties
import Data.Star.Vec
import Data.Stream
import Data.String
import Data.String.Base
import Data.Sum
import Data.Sum.Base
import Data.Sum.Properties
import Data.Sum.Relation.Core
import Data.Sum.Relation.LeftOrder
import Data.Sum.Relation.Pointwise
import Data.Table
import Data.Table.Base
import Data.Table.Properties
import Data.Table.Relation.Equality
import Data.Unit
import Data.Unit.Base
import Data.Unit.NonEta
import Data.Vec
import Data.Vec.All
import Data.Vec.All.Properties
import Data.Vec.Categorical
import Data.Vec.N-ary
import Data.Vec.Properties
import Data.Vec.Relation.Equality.DecPropositional
import Data.Vec.Relation.Equality.DecSetoid
import Data.Vec.Relation.Equality.Propositional
import Data.Vec.Relation.Equality.Setoid
import Data.Vec.Relation.Pointwise.Extensional
import Data.Vec.Relation.Pointwise.Inductive
import Data.W
import Data.W.Indexed
import Data.Word
import Foreign.Haskell
import Function
import Function.Bijection
import Function.Equality
import Function.Equivalence
import Function.Injection
import Function.Inverse
import Function.LeftInverse
import Function.Reasoning
import Function.Related
import Function.Related.TypeIsomorphisms
import Function.Surjection
import Induction
import Induction.Lexicographic
import Induction.Nat
import Induction.WellFounded
import IO
import IO.Primitive
import Level
import Record
import Reflection
import Relation.Binary
import Relation.Binary.Closure.Equivalence
import Relation.Binary.Closure.Reflexive
import Relation.Binary.Closure.ReflexiveTransitive
import Relation.Binary.Closure.ReflexiveTransitive.Properties
import Relation.Binary.Closure.Symmetric
import Relation.Binary.Closure.Transitive
import Relation.Binary.Consequences
import Relation.Binary.Core
import Relation.Binary.EqReasoning
import Relation.Binary.EquivalenceClosure
import Relation.Binary.Flip
import Relation.Binary.HeterogeneousEquality
import Relation.Binary.HeterogeneousEquality.Core
import Relation.Binary.HeterogeneousEquality.Quotients
import Relation.Binary.HeterogeneousEquality.Quotients.Examples
import Relation.Binary.Indexed
import Relation.Binary.Indexed.Core
import Relation.Binary.Indexed.Homogeneous
import Relation.Binary.InducedPreorders
import Relation.Binary.Lattice
import Relation.Binary.List.NonStrictLex
import Relation.Binary.List.Pointwise
import Relation.Binary.List.StrictLex
import Relation.Binary.NonStrictToStrict
import Relation.Binary.On
import Relation.Binary.OrderMorphism
import Relation.Binary.PartialOrderReasoning
import Relation.Binary.PreorderReasoning
import Relation.Binary.Product.NonStrictLex
import Relation.Binary.Product.Pointwise
import Relation.Binary.Product.StrictLex
import Relation.Binary.Properties.BoundedJoinSemilattice
import Relation.Binary.Properties.BoundedMeetSemilattice
import Relation.Binary.Properties.DecTotalOrder
import Relation.Binary.Properties.JoinSemilattice
import Relation.Binary.Properties.Lattice
import Relation.Binary.Properties.MeetSemilattice
import Relation.Binary.Properties.Poset
import Relation.Binary.Properties.Preorder
import Relation.Binary.Properties.StrictPartialOrder
import Relation.Binary.Properties.StrictTotalOrder
import Relation.Binary.Properties.TotalOrder
import Relation.Binary.PropositionalEquality
import Relation.Binary.PropositionalEquality.Core
import Relation.Binary.PropositionalEquality.TrustMe
import Relation.Binary.Reflection
import Relation.Binary.SetoidReasoning
import Relation.Binary.Sigma.Pointwise
import Relation.Binary.Simple
import Relation.Binary.StrictPartialOrderReasoning
import Relation.Binary.StrictToNonStrict
import Relation.Binary.Sum
import Relation.Binary.SymmetricClosure
import Relation.Binary.Vec.Pointwise
import Relation.Nullary
import Relation.Nullary.Decidable
import Relation.Nullary.Implication
import Relation.Nullary.Negation
import Relation.Nullary.Product
import Relation.Nullary.Sum
import Relation.Nullary.Universe
import Relation.Unary
import Relation.Unary.PredicateTransformer
import Relation.Unary.Properties
import Size
import Strict
import Universe