Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://agda.github.io/agda-stdlib/v2.0 below:

index

{-# OPTIONS --rewriting --sized-types --guardedness #-}

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.Apartness
import Algebra.Apartness.Bundles
import Algebra.Apartness.Properties.HeytingCommutativeRing
import Algebra.Apartness.Structures
import Algebra.Bundles
import Algebra.Bundles.Raw
import Algebra.Consequences.Base
import Algebra.Consequences.Propositional
import Algebra.Consequences.Setoid
import Algebra.Construct.Add.Identity
import Algebra.Construct.DirectProduct
import Algebra.Construct.Flip.Op
import Algebra.Construct.Initial
import Algebra.Construct.LexProduct
import Algebra.Construct.LexProduct.Base
import Algebra.Construct.LexProduct.Inner
import Algebra.Construct.LiftedChoice
import Algebra.Construct.NaturalChoice.Base
import Algebra.Construct.NaturalChoice.Max
import Algebra.Construct.NaturalChoice.MaxOp
import Algebra.Construct.NaturalChoice.Min
import Algebra.Construct.NaturalChoice.MinMaxOp
import Algebra.Construct.NaturalChoice.MinOp
import Algebra.Construct.Subst.Equality
import Algebra.Construct.Terminal
import Algebra.Construct.Zero
import Algebra.Core
import Algebra.Definitions
import Algebra.Definitions.RawMagma
import Algebra.Definitions.RawMonoid
import Algebra.Definitions.RawSemiring
import Algebra.Lattice
import Algebra.Lattice.Bundles
import Algebra.Lattice.Bundles.Raw
import Algebra.Lattice.Construct.DirectProduct
import Algebra.Lattice.Construct.LiftedChoice
import Algebra.Lattice.Construct.NaturalChoice.MaxOp
import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp
import Algebra.Lattice.Construct.NaturalChoice.MinOp
import Algebra.Lattice.Construct.Subst.Equality
import Algebra.Lattice.Construct.Zero
import Algebra.Lattice.Morphism
import Algebra.Lattice.Morphism.Construct.Composition
import Algebra.Lattice.Morphism.Construct.Identity
import Algebra.Lattice.Morphism.LatticeMonomorphism
import Algebra.Lattice.Morphism.Structures
import Algebra.Lattice.Properties.BooleanAlgebra
import Algebra.Lattice.Properties.BooleanAlgebra.Expression
import Algebra.Lattice.Properties.DistributiveLattice
import Algebra.Lattice.Properties.Lattice
import Algebra.Lattice.Properties.Semilattice
import Algebra.Lattice.Structures
import Algebra.Lattice.Structures.Biased
import Algebra.Module
import Algebra.Module.Bundles
import Algebra.Module.Consequences
import Algebra.Module.Construct.DirectProduct
import Algebra.Module.Construct.TensorUnit
import Algebra.Module.Construct.Zero
import Algebra.Module.Core
import Algebra.Module.Definitions
import Algebra.Module.Definitions.Bi
import Algebra.Module.Definitions.Bi.Simultaneous
import Algebra.Module.Definitions.Left
import Algebra.Module.Definitions.Right
import Algebra.Module.Morphism.Construct.Composition
import Algebra.Module.Morphism.Construct.Identity
import Algebra.Module.Morphism.Definitions
import Algebra.Module.Morphism.ModuleHomomorphism
import Algebra.Module.Morphism.Structures
import Algebra.Module.Properties
import Algebra.Module.Properties.Semimodule
import Algebra.Module.Structures
import Algebra.Module.Structures.Biased
import Algebra.Morphism
import Algebra.Morphism.Consequences
import Algebra.Morphism.Construct.Composition
import Algebra.Morphism.Construct.Identity
import Algebra.Morphism.Definitions
import Algebra.Morphism.GroupMonomorphism
import Algebra.Morphism.MagmaMonomorphism
import Algebra.Morphism.MonoidMonomorphism
import Algebra.Morphism.RingMonomorphism
import Algebra.Morphism.Structures
import Algebra.Properties.AbelianGroup
import Algebra.Properties.CancellativeCommutativeSemiring
import Algebra.Properties.CommutativeMagma.Divisibility
import Algebra.Properties.CommutativeMonoid
import Algebra.Properties.CommutativeMonoid.Mult
import Algebra.Properties.CommutativeMonoid.Mult.TCOptimised
import Algebra.Properties.CommutativeMonoid.Sum
import Algebra.Properties.CommutativeSemigroup
import Algebra.Properties.CommutativeSemigroup.Divisibility
import Algebra.Properties.CommutativeSemiring.Binomial
import Algebra.Properties.CommutativeSemiring.Exp
import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised
import Algebra.Properties.Group
import Algebra.Properties.KleeneAlgebra
import Algebra.Properties.Loop
import Algebra.Properties.Magma.Divisibility
import Algebra.Properties.MiddleBolLoop
import Algebra.Properties.Monoid.Divisibility
import Algebra.Properties.Monoid.Mult
import Algebra.Properties.Monoid.Mult.TCOptimised
import Algebra.Properties.Monoid.Sum
import Algebra.Properties.MoufangLoop
import Algebra.Properties.Quasigroup
import Algebra.Properties.Ring
import Algebra.Properties.RingWithoutOne
import Algebra.Properties.Semigroup
import Algebra.Properties.Semigroup.Divisibility
import Algebra.Properties.Semiring.Binomial
import Algebra.Properties.Semiring.Divisibility
import Algebra.Properties.Semiring.Exp
import Algebra.Properties.Semiring.Exp.TailRecursiveOptimised
import Algebra.Properties.Semiring.Exp.TCOptimised
import Algebra.Properties.Semiring.Mult
import Algebra.Properties.Semiring.Mult.TCOptimised
import Algebra.Properties.Semiring.Primality
import Algebra.Properties.Semiring.Sum
import Algebra.Solver.CommutativeMonoid
import Algebra.Solver.CommutativeMonoid.Example
import Algebra.Solver.IdempotentCommutativeMonoid
import Algebra.Solver.IdempotentCommutativeMonoid.Example
import Algebra.Solver.Monoid
import Algebra.Solver.Ring
import Algebra.Solver.Ring.AlmostCommutativeRing
import Algebra.Solver.Ring.Lemmas
import Algebra.Solver.Ring.NaturalCoefficients
import Algebra.Solver.Ring.NaturalCoefficients.Default
import Algebra.Solver.Ring.Simple
import Algebra.Structures
import Algebra.Structures.Biased
import Axiom.DoubleNegationElimination
import Axiom.ExcludedMiddle
import Axiom.Extensionality.Heterogeneous
import Axiom.Extensionality.Propositional
import Axiom.UniquenessOfIdentityProofs
import Axiom.UniquenessOfIdentityProofs.WithK
import Codata.Guarded.M
import Codata.Guarded.Stream
import Codata.Guarded.Stream.Properties
import Codata.Guarded.Stream.Relation.Binary.Pointwise
import Codata.Guarded.Stream.Relation.Unary.All
import Codata.Guarded.Stream.Relation.Unary.Any
import Codata.Musical.Cofin
import Codata.Musical.Colist
import Codata.Musical.Colist.Base
import Codata.Musical.Colist.Bisimilarity
import Codata.Musical.Colist.Infinite-merge
import Codata.Musical.Colist.Properties
import Codata.Musical.Colist.Relation.Unary.All
import Codata.Musical.Colist.Relation.Unary.All.Properties
import Codata.Musical.Colist.Relation.Unary.Any
import Codata.Musical.Colist.Relation.Unary.Any.Properties
import Codata.Musical.Conat
import Codata.Musical.Conat.Base
import Codata.Musical.Conversion
import Codata.Musical.Costring
import Codata.Musical.Covec
import Codata.Musical.M
import Codata.Musical.M.Indexed
import Codata.Musical.Notation
import Codata.Musical.Stream
import Codata.Sized.Cofin
import Codata.Sized.Cofin.Literals
import Codata.Sized.Colist
import Codata.Sized.Colist.Bisimilarity
import Codata.Sized.Colist.Effectful
import Codata.Sized.Colist.Properties
import Codata.Sized.Conat
import Codata.Sized.Conat.Bisimilarity
import Codata.Sized.Conat.Literals
import Codata.Sized.Conat.Properties
import Codata.Sized.Covec
import Codata.Sized.Covec.Bisimilarity
import Codata.Sized.Covec.Effectful
import Codata.Sized.Covec.Instances
import Codata.Sized.Covec.Properties
import Codata.Sized.Cowriter
import Codata.Sized.Cowriter.Bisimilarity
import Codata.Sized.Delay
import Codata.Sized.Delay.Bisimilarity
import Codata.Sized.Delay.Effectful
import Codata.Sized.Delay.Properties
import Codata.Sized.M
import Codata.Sized.M.Bisimilarity
import Codata.Sized.M.Properties
import Codata.Sized.Stream
import Codata.Sized.Stream.Bisimilarity
import Codata.Sized.Stream.Effectful
import Codata.Sized.Stream.Instances
import Codata.Sized.Stream.Properties
import Codata.Sized.Thunk
import Data.Bool
import Data.Bool.Base
import Data.Bool.Instances
import Data.Bool.Properties
import Data.Bool.Show
import Data.Bool.Solver
import Data.Char
import Data.Char.Base
import Data.Char.Instances
import Data.Char.Properties
import Data.Container
import Data.Container.Combinator
import Data.Container.Combinator.Properties
import Data.Container.Core
import Data.Container.Fixpoints.Guarded
import Data.Container.Fixpoints.Sized
import Data.Container.FreeMonad
import Data.Container.Indexed
import Data.Container.Indexed.Combinator
import Data.Container.Indexed.Core
import Data.Container.Indexed.Fixpoints.Guarded
import Data.Container.Indexed.FreeMonad
import Data.Container.Indexed.WithK
import Data.Container.Membership
import Data.Container.Morphism
import Data.Container.Morphism.Properties
import Data.Container.Properties
import Data.Container.Related
import Data.Container.Relation.Binary.Equality.Setoid
import Data.Container.Relation.Binary.Pointwise
import Data.Container.Relation.Binary.Pointwise.Properties
import Data.Container.Relation.Unary.All
import Data.Container.Relation.Unary.Any
import Data.Container.Relation.Unary.Any.Properties
import Data.Default
import Data.DifferenceList
import Data.DifferenceNat
import Data.DifferenceVec
import Data.Digit
import Data.Digit.Properties
import Data.Empty
import Data.Empty.Irrelevant
import Data.Empty.Polymorphic
import Data.Fin
import Data.Fin.Base
import Data.Fin.Induction
import Data.Fin.Instances
import Data.Fin.Literals
import Data.Fin.Patterns
import Data.Fin.Permutation
import Data.Fin.Permutation.Components
import Data.Fin.Permutation.Transposition.List
import Data.Fin.Properties
import Data.Fin.Reflection
import Data.Fin.Relation.Unary.Top
import Data.Fin.Show
import Data.Fin.Subset
import Data.Fin.Subset.Induction
import Data.Fin.Subset.Properties
import Data.Fin.Substitution
import Data.Fin.Substitution.Lemmas
import Data.Fin.Substitution.List
import Data.Float
import Data.Float.Base
import Data.Float.Instances
import Data.Float.Properties
import Data.Graph.Acyclic
import Data.Integer
import Data.Integer.Base
import Data.Integer.Coprimality
import Data.Integer.Divisibility
import Data.Integer.Divisibility.Signed
import Data.Integer.DivMod
import Data.Integer.GCD
import Data.Integer.Instances
import Data.Integer.LCM
import Data.Integer.Literals
import Data.Integer.Properties
import Data.Integer.Show
import Data.Integer.Solver
import Data.Integer.Tactic.RingSolver
import Data.Irrelevant
import Data.List
import Data.List.Base
import Data.List.Countdown
import Data.List.Effectful
import Data.List.Effectful.Transformer
import Data.List.Extrema
import Data.List.Extrema.Core
import Data.List.Extrema.Nat
import Data.List.Fresh
import Data.List.Fresh.Membership.Setoid
import Data.List.Fresh.Membership.Setoid.Properties
import Data.List.Fresh.NonEmpty
import Data.List.Fresh.Properties
import Data.List.Fresh.Relation.Unary.All
import Data.List.Fresh.Relation.Unary.All.Properties
import Data.List.Fresh.Relation.Unary.Any
import Data.List.Fresh.Relation.Unary.Any.Properties
import Data.List.Instances
import Data.List.Kleene
import Data.List.Kleene.AsList
import Data.List.Kleene.Base
import Data.List.Literals
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.Propositional.Properties.WithK
import Data.List.Membership.Setoid
import Data.List.Membership.Setoid.Properties
import Data.List.Nary.NonDependent
import Data.List.NonEmpty
import Data.List.NonEmpty.Base
import Data.List.NonEmpty.Effectful
import Data.List.NonEmpty.Effectful.Transformer
import Data.List.NonEmpty.Instances
import Data.List.NonEmpty.Properties
import Data.List.NonEmpty.Relation.Unary.All
import Data.List.Properties
import Data.List.Reflection
import Data.List.Relation.Binary.BagAndSetEquality
import Data.List.Relation.Binary.Disjoint.Propositional
import Data.List.Relation.Binary.Disjoint.Setoid
import Data.List.Relation.Binary.Disjoint.Setoid.Properties
import Data.List.Relation.Binary.Equality.DecPropositional
import Data.List.Relation.Binary.Equality.DecSetoid
import Data.List.Relation.Binary.Equality.Propositional
import Data.List.Relation.Binary.Equality.Setoid
import Data.List.Relation.Binary.Infix.Heterogeneous
import Data.List.Relation.Binary.Infix.Heterogeneous.Properties
import Data.List.Relation.Binary.Infix.Homogeneous.Properties
import Data.List.Relation.Binary.Lex
import Data.List.Relation.Binary.Lex.Core
import Data.List.Relation.Binary.Lex.NonStrict
import Data.List.Relation.Binary.Lex.Strict
import Data.List.Relation.Binary.Permutation.Homogeneous
import Data.List.Relation.Binary.Permutation.Propositional
import Data.List.Relation.Binary.Permutation.Propositional.Properties
import Data.List.Relation.Binary.Permutation.Setoid
import Data.List.Relation.Binary.Permutation.Setoid.Properties
import Data.List.Relation.Binary.Pointwise
import Data.List.Relation.Binary.Pointwise.Base
import Data.List.Relation.Binary.Pointwise.Properties
import Data.List.Relation.Binary.Prefix.Heterogeneous
import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties
import Data.List.Relation.Binary.Prefix.Homogeneous.Properties
import Data.List.Relation.Binary.Sublist.DecPropositional
import Data.List.Relation.Binary.Sublist.DecPropositional.Solver
import Data.List.Relation.Binary.Sublist.DecSetoid
import Data.List.Relation.Binary.Sublist.DecSetoid.Solver
import Data.List.Relation.Binary.Sublist.Heterogeneous
import Data.List.Relation.Binary.Sublist.Heterogeneous.Core
import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
import Data.List.Relation.Binary.Sublist.Heterogeneous.Solver
import Data.List.Relation.Binary.Sublist.Propositional
import Data.List.Relation.Binary.Sublist.Propositional.Disjoint
import Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables
import Data.List.Relation.Binary.Sublist.Propositional.Properties
import Data.List.Relation.Binary.Sublist.Setoid
import Data.List.Relation.Binary.Sublist.Setoid.Properties
import Data.List.Relation.Binary.Subset.Propositional
import Data.List.Relation.Binary.Subset.Propositional.Properties
import Data.List.Relation.Binary.Subset.Setoid
import Data.List.Relation.Binary.Subset.Setoid.Properties
import Data.List.Relation.Binary.Suffix.Heterogeneous
import Data.List.Relation.Binary.Suffix.Heterogeneous.Properties
import Data.List.Relation.Binary.Suffix.Homogeneous.Properties
import Data.List.Relation.Ternary.Appending
import Data.List.Relation.Ternary.Appending.Properties
import Data.List.Relation.Ternary.Appending.Propositional
import Data.List.Relation.Ternary.Appending.Propositional.Properties
import Data.List.Relation.Ternary.Appending.Setoid
import Data.List.Relation.Ternary.Appending.Setoid.Properties
import Data.List.Relation.Ternary.Interleaving
import Data.List.Relation.Ternary.Interleaving.Properties
import Data.List.Relation.Ternary.Interleaving.Propositional
import Data.List.Relation.Ternary.Interleaving.Propositional.Properties
import Data.List.Relation.Ternary.Interleaving.Setoid
import Data.List.Relation.Ternary.Interleaving.Setoid.Properties
import Data.List.Relation.Unary.All
import Data.List.Relation.Unary.AllPairs
import Data.List.Relation.Unary.AllPairs.Core
import Data.List.Relation.Unary.AllPairs.Properties
import Data.List.Relation.Unary.All.Properties
import Data.List.Relation.Unary.Any
import Data.List.Relation.Unary.Any.Properties
import Data.List.Relation.Unary.Enumerates.Setoid
import Data.List.Relation.Unary.Enumerates.Setoid.Properties
import Data.List.Relation.Unary.First
import Data.List.Relation.Unary.First.Properties
import Data.List.Relation.Unary.Grouped
import Data.List.Relation.Unary.Grouped.Properties
import Data.List.Relation.Unary.Linked
import Data.List.Relation.Unary.Linked.Properties
import Data.List.Relation.Unary.Sorted.TotalOrder
import Data.List.Relation.Unary.Sorted.TotalOrder.Properties
import Data.List.Relation.Unary.Sufficient
import Data.List.Relation.Unary.Unique.DecPropositional
import Data.List.Relation.Unary.Unique.DecPropositional.Properties
import Data.List.Relation.Unary.Unique.DecSetoid
import Data.List.Relation.Unary.Unique.DecSetoid.Properties
import Data.List.Relation.Unary.Unique.Propositional
import Data.List.Relation.Unary.Unique.Propositional.Properties
import Data.List.Relation.Unary.Unique.Setoid
import Data.List.Relation.Unary.Unique.Setoid.Properties
import Data.List.Reverse
import Data.List.Sort
import Data.List.Sort.Base
import Data.List.Sort.MergeSort
import Data.List.Zipper
import Data.List.Zipper.Properties
import Data.Maybe
import Data.Maybe.Base
import Data.Maybe.Effectful
import Data.Maybe.Effectful.Transformer
import Data.Maybe.Instances
import Data.Maybe.Properties
import Data.Maybe.Relation.Binary.Connected
import Data.Maybe.Relation.Binary.Pointwise
import Data.Maybe.Relation.Unary.All
import Data.Maybe.Relation.Unary.All.Properties
import Data.Maybe.Relation.Unary.Any
import Data.Nat
import Data.Nat.Base
import Data.Nat.Binary
import Data.Nat.Binary.Base
import Data.Nat.Binary.Induction
import Data.Nat.Binary.Instances
import Data.Nat.Binary.Properties
import Data.Nat.Binary.Subtraction
import Data.Nat.Combinatorics
import Data.Nat.Combinatorics.Base
import Data.Nat.Combinatorics.Specification
import Data.Nat.Coprimality
import Data.Nat.Divisibility
import Data.Nat.Divisibility.Core
import Data.Nat.DivMod
import Data.Nat.DivMod.Core
import Data.Nat.DivMod.WithK
import Data.Nat.GCD
import Data.Nat.GCD.Lemmas
import Data.Nat.GeneralisedArithmetic
import Data.Nat.Induction
import Data.Nat.InfinitelyOften
import Data.Nat.Instances
import Data.Nat.LCM
import Data.Nat.Literals
import Data.Nat.Logarithm
import Data.Nat.Logarithm.Core
import Data.Nat.Primality
import Data.Nat.Properties
import Data.Nat.PseudoRandom.LCG
import Data.Nat.PseudoRandom.LCG.Unsafe
import Data.Nat.Reflection
import Data.Nat.Show
import Data.Nat.Show.Properties
import Data.Nat.Solver
import Data.Nat.Tactic.RingSolver
import Data.Nat.WithK
import Data.Parity
import Data.Parity.Base
import Data.Parity.Instances
import Data.Parity.Properties
import Data.Product
import Data.Product.Algebra
import Data.Product.Base
import Data.Product.Effectful.Examples
import Data.Product.Effectful.Left
import Data.Product.Effectful.Left.Base
import Data.Product.Effectful.Right
import Data.Product.Effectful.Right.Base
import Data.Product.Function.Dependent.Propositional
import Data.Product.Function.Dependent.Propositional.WithK
import Data.Product.Function.Dependent.Setoid
import Data.Product.Function.NonDependent.Propositional
import Data.Product.Function.NonDependent.Setoid
import Data.Product.Instances
import Data.Product.Nary.NonDependent
import Data.Product.Properties
import Data.Product.Properties.WithK
import Data.Product.Relation.Binary.Lex.NonStrict
import Data.Product.Relation.Binary.Lex.Strict
import Data.Product.Relation.Binary.Pointwise.Dependent
import Data.Product.Relation.Binary.Pointwise.Dependent.WithK
import Data.Product.Relation.Binary.Pointwise.NonDependent
import Data.Product.Relation.Unary.All
import Data.Rational
import Data.Rational.Base
import Data.Rational.Instances
import Data.Rational.Literals
import Data.Rational.Properties
import Data.Rational.Show
import Data.Rational.Solver
import Data.Rational.Unnormalised
import Data.Rational.Unnormalised.Base
import Data.Rational.Unnormalised.Properties
import Data.Rational.Unnormalised.Show
import Data.Rational.Unnormalised.Solver
import Data.Record
import Data.Refinement
import Data.Refinement.Relation.Unary.All
import Data.Sign
import Data.Sign.Base
import Data.Sign.Instances
import Data.Sign.Properties
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.Vec
import Data.String
import Data.String.Base
import Data.String.Instances
import Data.String.Literals
import Data.String.Properties
import Data.String.Unsafe
import Data.Sum
import Data.Sum.Algebra
import Data.Sum.Base
import Data.Sum.Effectful.Examples
import Data.Sum.Effectful.Left
import Data.Sum.Effectful.Left.Transformer
import Data.Sum.Effectful.Right
import Data.Sum.Effectful.Right.Transformer
import Data.Sum.Function.Propositional
import Data.Sum.Function.Setoid
import Data.Sum.Instances
import Data.Sum.Properties
import Data.Sum.Relation.Binary.LeftOrder
import Data.Sum.Relation.Binary.Pointwise
import Data.Sum.Relation.Unary.All
import Data.These
import Data.These.Base
import Data.These.Effectful.Left
import Data.These.Effectful.Left.Base
import Data.These.Effectful.Right
import Data.These.Effectful.Right.Base
import Data.These.Instances
import Data.These.Properties
import Data.Tree.AVL
import Data.Tree.AVL.Height
import Data.Tree.AVL.Indexed
import Data.Tree.AVL.IndexedMap
import Data.Tree.AVL.Indexed.Relation.Unary.All
import Data.Tree.AVL.Indexed.Relation.Unary.Any
import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties
import Data.Tree.AVL.Indexed.WithK
import Data.Tree.AVL.Key
import Data.Tree.AVL.Map
import Data.Tree.AVL.Map.Membership.Propositional
import Data.Tree.AVL.Map.Membership.Propositional.Properties
import Data.Tree.AVL.Map.Relation.Unary.Any
import Data.Tree.AVL.NonEmpty
import Data.Tree.AVL.NonEmpty.Propositional
import Data.Tree.AVL.Relation.Unary.Any
import Data.Tree.AVL.Sets
import Data.Tree.AVL.Sets.Membership
import Data.Tree.AVL.Sets.Membership.Properties
import Data.Tree.AVL.Value
import Data.Tree.Binary
import Data.Tree.Binary.Properties
import Data.Tree.Binary.Relation.Unary.All
import Data.Tree.Binary.Relation.Unary.All.Properties
import Data.Tree.Binary.Show
import Data.Tree.Binary.Zipper
import Data.Tree.Binary.Zipper.Properties
import Data.Tree.Rose
import Data.Tree.Rose.Properties
import Data.Tree.Rose.Show
import Data.Trie
import Data.Trie.NonEmpty
import Data.Unit
import Data.Unit.Base
import Data.Unit.Instances
import Data.Unit.NonEta
import Data.Unit.Polymorphic
import Data.Unit.Polymorphic.Base
import Data.Unit.Polymorphic.Instances
import Data.Unit.Polymorphic.Properties
import Data.Unit.Properties
import Data.Universe
import Data.Universe.Indexed
import Data.Vec
import Data.Vec.Base
import Data.Vec.Bounded
import Data.Vec.Bounded.Base
import Data.Vec.Effectful
import Data.Vec.Effectful.Transformer
import Data.Vec.Functional
import Data.Vec.Functional.Properties
import Data.Vec.Functional.Relation.Binary.Equality.Setoid
import Data.Vec.Functional.Relation.Binary.Pointwise
import Data.Vec.Functional.Relation.Binary.Pointwise.Properties
import Data.Vec.Functional.Relation.Unary.All
import Data.Vec.Functional.Relation.Unary.All.Properties
import Data.Vec.Functional.Relation.Unary.Any
import Data.Vec.Instances
import Data.Vec.Membership.DecPropositional
import Data.Vec.Membership.DecSetoid
import Data.Vec.Membership.Propositional
import Data.Vec.Membership.Propositional.Properties
import Data.Vec.Membership.Setoid
import Data.Vec.N-ary
import Data.Vec.Properties
import Data.Vec.Properties.WithK
import Data.Vec.Recursive
import Data.Vec.Recursive.Effectful
import Data.Vec.Recursive.Properties
import Data.Vec.Reflection
import Data.Vec.Relation.Binary.Equality.Cast
import Data.Vec.Relation.Binary.Equality.DecPropositional
import Data.Vec.Relation.Binary.Equality.DecSetoid
import Data.Vec.Relation.Binary.Equality.Propositional
import Data.Vec.Relation.Binary.Equality.Propositional.WithK
import Data.Vec.Relation.Binary.Equality.Setoid
import Data.Vec.Relation.Binary.Lex.Core
import Data.Vec.Relation.Binary.Lex.NonStrict
import Data.Vec.Relation.Binary.Lex.Strict
import Data.Vec.Relation.Binary.Pointwise.Extensional
import Data.Vec.Relation.Binary.Pointwise.Inductive
import Data.Vec.Relation.Unary.All
import Data.Vec.Relation.Unary.AllPairs
import Data.Vec.Relation.Unary.AllPairs.Core
import Data.Vec.Relation.Unary.AllPairs.Properties
import Data.Vec.Relation.Unary.All.Properties
import Data.Vec.Relation.Unary.Any
import Data.Vec.Relation.Unary.Any.Properties
import Data.Vec.Relation.Unary.Linked
import Data.Vec.Relation.Unary.Linked.Properties
import Data.Vec.Relation.Unary.Unique.Propositional
import Data.Vec.Relation.Unary.Unique.Propositional.Properties
import Data.Vec.Relation.Unary.Unique.Setoid
import Data.Vec.Relation.Unary.Unique.Setoid.Properties
import Data.W
import Data.W.Indexed
import Data.Word
import Data.Word.Base
import Data.Word.Instances
import Data.Word.Properties
import Data.Wrap
import Data.W.Sized
import Data.W.WithK
import Debug.Trace
import Effect.Applicative
import Effect.Applicative.Indexed
import Effect.Applicative.Predicate
import Effect.Choice
import Effect.Comonad
import Effect.Empty
import Effect.Functor
import Effect.Functor.Predicate
import Effect.Monad
import Effect.Monad.Continuation
import Effect.Monad.Error.Transformer
import Effect.Monad.Identity
import Effect.Monad.Identity.Instances
import Effect.Monad.Indexed
import Effect.Monad.IO
import Effect.Monad.IO.Instances
import Effect.Monad.Partiality
import Effect.Monad.Partiality.All
import Effect.Monad.Partiality.Instances
import Effect.Monad.Predicate
import Effect.Monad.Reader
import Effect.Monad.Reader.Indexed
import Effect.Monad.Reader.Instances
import Effect.Monad.Reader.Transformer
import Effect.Monad.Reader.Transformer.Base
import Effect.Monad.State
import Effect.Monad.State.Indexed
import Effect.Monad.State.Instances
import Effect.Monad.State.Transformer
import Effect.Monad.State.Transformer.Base
import Effect.Monad.Writer
import Effect.Monad.Writer.Indexed
import Effect.Monad.Writer.Instances
import Effect.Monad.Writer.Transformer
import Effect.Monad.Writer.Transformer.Base
import Foreign.Haskell
import Foreign.Haskell.Coerce
import Foreign.Haskell.Either
import Foreign.Haskell.List.NonEmpty
import Foreign.Haskell.Pair
import Function
import Function.Base
import Function.Bundles
import Function.Consequences
import Function.Consequences.Propositional
import Function.Consequences.Setoid
import Function.Construct.Composition
import Function.Construct.Constant
import Function.Construct.Identity
import Function.Construct.Symmetry
import Function.Core
import Function.Definitions
import Function.Dependent.Bundles
import Function.Endomorphism.Propositional
import Function.Endomorphism.Setoid
import Function.Identity.Effectful
import Function.Indexed.Bundles
import Function.Indexed.Relation.Binary.Equality
import Function.Metric
import Function.Metric.Bundles
import Function.Metric.Core
import Function.Metric.Definitions
import Function.Metric.Nat
import Function.Metric.Nat.Bundles
import Function.Metric.Nat.Core
import Function.Metric.Nat.Definitions
import Function.Metric.Nat.Structures
import Function.Metric.Rational
import Function.Metric.Rational.Bundles
import Function.Metric.Rational.Core
import Function.Metric.Rational.Definitions
import Function.Metric.Rational.Structures
import Function.Metric.Structures
import Function.Nary.NonDependent
import Function.Nary.NonDependent.Base
import Function.Properties
import Function.Properties.Bijection
import Function.Properties.Equivalence
import Function.Properties.Injection
import Function.Properties.Inverse
import Function.Properties.Inverse.HalfAdjointEquivalence
import Function.Properties.RightInverse
import Function.Properties.Surjection
import Function.Reasoning
import Function.Related.Propositional
import Function.Related.TypeIsomorphisms
import Function.Related.TypeIsomorphisms.Solver
import Function.Strict
import Function.Structures
import Function.Structures.Biased
import Induction
import Induction.Lexicographic
import Induction.WellFounded
import IO
import IO.Base
import IO.Effectful
import IO.Finite
import IO.Infinite
import IO.Instances
import IO.Primitive
import IO.Primitive.Finite
import IO.Primitive.Infinite
import Level
import Level.Literals
import Reflection
import Reflection.AnnotatedAST
import Reflection.AnnotatedAST.Free
import Reflection.AST.Abstraction
import Reflection.AST
import Reflection.AST.AlphaEquality
import Reflection.AST.Argument
import Reflection.AST.Argument.Information
import Reflection.AST.Argument.Modality
import Reflection.AST.Argument.Quantity
import Reflection.AST.Argument.Relevance
import Reflection.AST.Argument.Visibility
import Reflection.AST.DeBruijn
import Reflection.AST.Definition
import Reflection.AST.Instances
import Reflection.AST.Literal
import Reflection.AST.Meta
import Reflection.AST.Name
import Reflection.AST.Pattern
import Reflection.AST.Show
import Reflection.AST.Term
import Reflection.AST.Traversal
import Reflection.AST.Universe
import Reflection.External
import Reflection.TCM
import Reflection.TCM.Effectful
import Reflection.TCM.Format
import Reflection.TCM.Instances
import Reflection.TCM.Syntax
import Relation.Binary
import Relation.Binary.Bundles
import Relation.Binary.Consequences
import Relation.Binary.Construct.Add.Extrema.Equality
import Relation.Binary.Construct.Add.Extrema.NonStrict
import Relation.Binary.Construct.Add.Extrema.Strict
import Relation.Binary.Construct.Add.Infimum.Equality
import Relation.Binary.Construct.Add.Infimum.NonStrict
import Relation.Binary.Construct.Add.Infimum.Strict
import Relation.Binary.Construct.Add.Point.Equality
import Relation.Binary.Construct.Add.Supremum.Equality
import Relation.Binary.Construct.Add.Supremum.NonStrict
import Relation.Binary.Construct.Add.Supremum.Strict
import Relation.Binary.Construct.Always
import Relation.Binary.Construct.Closure.Equivalence
import Relation.Binary.Construct.Closure.Equivalence.Properties
import Relation.Binary.Construct.Closure.Reflexive
import Relation.Binary.Construct.Closure.Reflexive.Properties
import Relation.Binary.Construct.Closure.Reflexive.Properties.WithK
import Relation.Binary.Construct.Closure.ReflexiveTransitive
import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties.WithK
import Relation.Binary.Construct.Closure.Symmetric
import Relation.Binary.Construct.Closure.SymmetricTransitive
import Relation.Binary.Construct.Closure.Transitive
import Relation.Binary.Construct.Closure.Transitive.WithK
import Relation.Binary.Construct.Composition
import Relation.Binary.Construct.Constant
import Relation.Binary.Construct.Constant.Core
import Relation.Binary.Construct.Flip.EqAndOrd
import Relation.Binary.Construct.Flip.Ord
import Relation.Binary.Construct.FromPred
import Relation.Binary.Construct.FromRel
import Relation.Binary.Construct.Intersection
import Relation.Binary.Construct.NaturalOrder.Left
import Relation.Binary.Construct.NaturalOrder.Right
import Relation.Binary.Construct.Never
import Relation.Binary.Construct.NonStrictToStrict
import Relation.Binary.Construct.On
import Relation.Binary.Construct.StrictToNonStrict
import Relation.Binary.Construct.Subst.Equality
import Relation.Binary.Construct.Union
import Relation.Binary.Core
import Relation.Binary.Definitions
import Relation.Binary.HeterogeneousEquality
import Relation.Binary.HeterogeneousEquality.Core
import Relation.Binary.HeterogeneousEquality.Quotients
import Relation.Binary.HeterogeneousEquality.Quotients.Examples
import Relation.Binary.Indexed.Heterogeneous
import Relation.Binary.Indexed.Heterogeneous.Bundles
import Relation.Binary.Indexed.Heterogeneous.Construct.At
import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
import Relation.Binary.Indexed.Heterogeneous.Core
import Relation.Binary.Indexed.Heterogeneous.Definitions
import Relation.Binary.Indexed.Heterogeneous.Structures
import Relation.Binary.Indexed.Homogeneous
import Relation.Binary.Indexed.Homogeneous.Bundles
import Relation.Binary.Indexed.Homogeneous.Construct.At
import Relation.Binary.Indexed.Homogeneous.Core
import Relation.Binary.Indexed.Homogeneous.Definitions
import Relation.Binary.Indexed.Homogeneous.Structures
import Relation.Binary.Lattice
import Relation.Binary.Lattice.Bundles
import Relation.Binary.Lattice.Definitions
import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice
import Relation.Binary.Lattice.Properties.BoundedLattice
import Relation.Binary.Lattice.Properties.BoundedMeetSemilattice
import Relation.Binary.Lattice.Properties.DistributiveLattice
import Relation.Binary.Lattice.Properties.HeytingAlgebra
import Relation.Binary.Lattice.Properties.JoinSemilattice
import Relation.Binary.Lattice.Properties.Lattice
import Relation.Binary.Lattice.Properties.MeetSemilattice
import Relation.Binary.Lattice.Structures
import Relation.Binary.Morphism
import Relation.Binary.Morphism.Bundles
import Relation.Binary.Morphism.Construct.Composition
import Relation.Binary.Morphism.Construct.Constant
import Relation.Binary.Morphism.Construct.Identity
import Relation.Binary.Morphism.Definitions
import Relation.Binary.Morphism.OrderMonomorphism
import Relation.Binary.Morphism.RelMonomorphism
import Relation.Binary.Morphism.Structures
import Relation.Binary.Properties.ApartnessRelation
import Relation.Binary.Properties.DecTotalOrder
import Relation.Binary.Properties.Poset
import Relation.Binary.Properties.Preorder
import Relation.Binary.Properties.Setoid
import Relation.Binary.Properties.StrictPartialOrder
import Relation.Binary.Properties.StrictTotalOrder
import Relation.Binary.Properties.TotalOrder
import Relation.Binary.PropositionalEquality
import Relation.Binary.PropositionalEquality.Algebra
import Relation.Binary.PropositionalEquality.Core
import Relation.Binary.PropositionalEquality.Properties
import Relation.Binary.PropositionalEquality.TrustMe
import Relation.Binary.PropositionalEquality.WithK
import Relation.Binary.Reasoning.Base.Apartness
import Relation.Binary.Reasoning.Base.Double
import Relation.Binary.Reasoning.Base.Partial
import Relation.Binary.Reasoning.Base.Single
import Relation.Binary.Reasoning.Base.Triple
import Relation.Binary.Reasoning.MultiSetoid
import Relation.Binary.Reasoning.PartialOrder
import Relation.Binary.Reasoning.PartialSetoid
import Relation.Binary.Reasoning.Preorder
import Relation.Binary.Reasoning.Setoid
import Relation.Binary.Reasoning.StrictPartialOrder
import Relation.Binary.Reasoning.Syntax
import Relation.Binary.Reflection
import Relation.Binary.Rewriting
import Relation.Binary.Structures
import Relation.Binary.Structures.Biased
import Relation.Binary.TypeClasses
import Relation.Nary
import Relation.Nullary
import Relation.Nullary.Construct.Add.Extrema
import Relation.Nullary.Construct.Add.Infimum
import Relation.Nullary.Construct.Add.Point
import Relation.Nullary.Construct.Add.Supremum
import Relation.Nullary.Decidable
import Relation.Nullary.Decidable.Core
import Relation.Nullary.Indexed
import Relation.Nullary.Indexed.Negation
import Relation.Nullary.Negation
import Relation.Nullary.Negation.Core
import Relation.Nullary.Reflects
import Relation.Nullary.Universe
import Relation.Unary
import Relation.Unary.Algebra
import Relation.Unary.Closure.Base
import Relation.Unary.Closure.Preorder
import Relation.Unary.Closure.StrictPartialOrder
import Relation.Unary.Consequences
import Relation.Unary.Indexed
import Relation.Unary.Polymorphic
import Relation.Unary.Polymorphic.Properties
import Relation.Unary.PredicateTransformer
import Relation.Unary.Properties
import Relation.Unary.Relation.Binary.Equality
import Relation.Unary.Relation.Binary.Subset
import Relation.Unary.Sized
import Size
import System.Clock
import System.Clock.Primitive
import System.Console.ANSI
import System.Directory
import System.Directory.Primitive
import System.Environment
import System.Environment.Primitive
import System.Exit
import System.Exit.Primitive
import System.FilePath.Posix
import System.FilePath.Posix.Primitive
import System.Process
import System.Process.Primitive
import Tactic.Cong
import Tactic.MonoidSolver
import Tactic.RingSolver
import Tactic.RingSolver.Core.AlmostCommutativeRing
import Tactic.RingSolver.Core.Expression
import Tactic.RingSolver.Core.NatSet
import Tactic.RingSolver.Core.Polynomial.Base
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition
import Tactic.RingSolver.Core.Polynomial.Homomorphism
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation
import Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables
import Tactic.RingSolver.Core.Polynomial.Parameters
import Tactic.RingSolver.Core.Polynomial.Reasoning
import Tactic.RingSolver.Core.Polynomial.Semantics
import Tactic.RingSolver.NonReflective
import Test.Golden
import Text.Format
import Text.Format.Generic
import Text.Pretty
import Text.Pretty.Core
import Text.Printf
import Text.Printf.Generic
import Text.Regex
import Text.Regex.Base
import Text.Regex.Derivative.Brzozowski
import Text.Regex.Properties
import Text.Regex.Properties.Core
import Text.Regex.Search
import Text.Regex.SmartConstructors
import Text.Regex.String
import Text.Regex.String.Unsafe
import Text.Tabular.Base
import Text.Tabular.List
import Text.Tabular.Vec

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4