{-# OPTIONS --without-K --exact-split --rewriting #-}

module index where

-- An organised list of modules:
import Pi.Everything

-- An exhaustive list of all modules:
import Pi.Common.Arithmetic
import Pi.Common.Extra
import Pi.Common.FinHelpers
import Pi.Common.InequalityEquiv
import Pi.Common.LList
import Pi.Common.ListFinLListEquiv
import Pi.Common.ListN
import Pi.Common.Misc
import Pi.Coxeter.Coxeter
import Pi.Coxeter.GeneratedGroup
import Pi.Coxeter.GeneratedGroupGeneralised
import Pi.Coxeter.GeneratedGroupIso
import Pi.Coxeter.GeneratedGroupIsoGeneralised
import Pi.Coxeter.Group
import Pi.Coxeter.InvTransform
import Pi.Coxeter.Lehmer2CoxeterEquiv
import Pi.Coxeter.Lehmer2SnEquiv
import Pi.Coxeter.LehmerCoxeterEquiv
import Pi.Coxeter.LehmerImmersion
import Pi.Coxeter.LehmerSnEquiv
import Pi.Coxeter.NonParametrized.Coxeter
import Pi.Coxeter.NonParametrized.CoxeterMCoxeterEquiv
import Pi.Coxeter.NonParametrized.CritPairsLong
import Pi.Coxeter.NonParametrized.Diamond
import Pi.Coxeter.NonParametrized.ExchangeLemmas+
import Pi.Coxeter.NonParametrized.ExchangeLemmas
import Pi.Coxeter.NonParametrized.ImpossibleLists
import Pi.Coxeter.NonParametrized.LehmerCanonical
import Pi.Coxeter.NonParametrized.LehmerReduction
import Pi.Coxeter.NonParametrized.MCoxeter
import Pi.Coxeter.NonParametrized.MCoxeterS
import Pi.Coxeter.NonParametrized.ReductionRel+
import Pi.Coxeter.NonParametrized.ReductionRel
import Pi.Coxeter.Norm
import Pi.Coxeter.NormEquiv
import Pi.Coxeter.Parametrized.CoxeterMCoxeterEquiv
import Pi.Coxeter.Parametrized.MCoxeter
import Pi.Coxeter.Parametrized.ReductionRel
import Pi.Coxeter.Sn
import Pi.Equiv.Equiv0
import Pi.Equiv.Equiv0Hat
import Pi.Equiv.Equiv0Norm
import Pi.Equiv.Equiv1
import Pi.Equiv.Equiv1Hat
import Pi.Equiv.Equiv1Norm
import Pi.Equiv.Equiv1NormHelpers
import Pi.Equiv.Equiv2
import Pi.Equiv.Equiv2Hat
import Pi.Equiv.Equiv2HatHelpers
import Pi.Equiv.Equiv2Norm
import Pi.Equiv.Translation2
import Pi.Everything
import Pi.Examples.Adder
import Pi.Examples.Base
import Pi.Examples.Copy
import Pi.Examples.Examples
import Pi.Examples.ExpMod
import Pi.Examples.Incr
import Pi.Examples.Interp
import Pi.Examples.Reset
import Pi.Examples.Toffoli
import Pi.Experiments.CoxeterHIT
import Pi.Experiments.Equiv.Equiv0
import Pi.Experiments.Equiv.Equiv1
import Pi.Experiments.Equiv.Equiv1Norm
import Pi.Experiments.Equiv.Equiv2
import Pi.Experiments.Equiv.Level0
import Pi.Experiments.Equiv.Util
import Pi.Experiments.PiLevel0
import Pi.Experiments.ShiftHIT
import Pi.Experiments.Translation
import Pi.FSMG.Conjectures
import Pi.FSMG.FSMG
import Pi.FSMG.FSMG.Properties
import Pi.FSMG.M
import Pi.FSMG.M.Properties
import Pi.FSMG.Paths
import Pi.FSMG.SMG
import Pi.FSMG.UFin
import Pi.Lehmer.FinExcept
import Pi.Lehmer.Lehmer
import Pi.Lehmer.Lehmer2
import Pi.Lehmer.Lehmer2FinEquiv
import Pi.Lehmer.LehmerFinEquiv
import Pi.Syntax.Pi+.Indexed
import Pi.Syntax.Pi+.NonIndexed
import Pi.Syntax.Pi
import Pi.Syntax.Pi^
import Pi.Syntax.Pi^Helpers
import Pi.UFin.BAut
import Pi.UFin.Base
import Pi.UFin.Misc
import Pi.UFin.Monoidal
import Pi.UFin.Paths
import Pi.UFin.UFin
import Pi.UFin.UFinLehmer2Equiv
import Pi.UFin.UFinLehmerEquiv
import Pi.UFin.Univ