Skip to content

Instantly share code, notes, and snippets.

@andy0130tw
Created November 29, 2023 15:02
Show Gist options
  • Save andy0130tw/f964b5a95c45204e3a99b8378de24d75 to your computer and use it in GitHub Desktop.
Save andy0130tw/f964b5a95c45204e3a99b8378de24d75 to your computer and use it in GitHub Desktop.
agda-stdlib's Everything v1.7.3
------------------------------------------------------------------------
-- The Agda standard library
--
-- All library modules, along with short descriptions
------------------------------------------------------------------------
-- Note that core modules are not included.
{-# OPTIONS --rewriting --guardedness --sized-types #-}
module Everything where
-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
import Algebra
-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
import Algebra.Bundles
-- Lemmas relating algebraic definitions (such as associativity and
-- commutativity) that don't 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
-- 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
-- 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 ordering.
import Algebra.Construct.NaturalChoice.Base
-- The max operator derived from an arbitrary total order
import Algebra.Construct.NaturalChoice.Max
-- Properties of a max operator derived from a spec over a total order.
import Algebra.Construct.NaturalChoice.MaxOp
-- The min operator derived from an arbitrary total order
import Algebra.Construct.NaturalChoice.Min
-- Properties of min and max operators specified over a total order
import Algebra.Construct.NaturalChoice.MinMaxOp
-- Properties of a min operator derived from a spec over a total order.
import Algebra.Construct.NaturalChoice.MinOp
-- 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.
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 defined over some other
-- structure, like modules and vector spaces
import Algebra.Module.Bundles
-- 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
-- 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 of left-scaling
import Algebra.Module.Definitions.Left
-- Properties of right-scaling
import Algebra.Module.Definitions.Right
-- 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
-- Some properties of Magma homomorphisms
import Algebra.Morphism.Consequences
-- 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 lattice-like structures
import Algebra.Morphism.LatticeMonomorphism
-- 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 derivable properties
import Algebra.Properties.BooleanAlgebra
-- Boolean algebra expressions
import Algebra.Properties.BooleanAlgebra.Expression
-- 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
-- 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.DistributiveLattice
-- Some derivable properties
import Algebra.Properties.Group
-- Some derivable properties
import Algebra.Properties.Lattice
-- Divisibility over magmas
import Algebra.Properties.Magma.Divisibility
-- 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 basic properties of Rings
import Algebra.Properties.Ring
-- Some theory for Semigroup
import Algebra.Properties.Semigroup
-- Properties of divisibility over semigroups
import Algebra.Properties.Semigroup.Divisibility
-- Some derivable properties
import Algebra.Properties.Semilattice
-- 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
-- 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
-- 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
-- A solver for equations over monoids
import Algebra.Solver.Monoid
-- 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
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
-- Applicative functors
import Category.Applicative
-- Indexed applicative functors
import Category.Applicative.Indexed
-- Applicative functors on indexed sets (predicates)
import Category.Applicative.Predicate
-- Comonads
import Category.Comonad
-- Functors
import Category.Functor
-- Functors on indexed sets (predicates)
import Category.Functor.Predicate
-- Monads
import Category.Monad
-- A delimited continuation monad
import Category.Monad.Continuation
-- Indexed monads
import Category.Monad.Indexed
-- The partiality monad
import Category.Monad.Partiality
-- An All predicate for the partiality monad
import Category.Monad.Partiality.All
-- Typeclass instances for _⊥
import Category.Monad.Partiality.Instances
-- Monads on indexed sets (predicates)
import Category.Monad.Predicate
-- The reader monad
import Category.Monad.Reader
-- The state monad
import Category.Monad.State
-- "Finite" sets indexed on coinductive "natural" numbers
import Codata.Cofin
-- Conat Literals
import Codata.Cofin.Literals
-- The Colist type and some operations
import Codata.Colist
-- Bisimilarity for Colists
import Codata.Colist.Bisimilarity
-- A categorical view of Colist
import Codata.Colist.Categorical
-- Properties of operations on the Colist type
import Codata.Colist.Properties
-- The Conat type and some operations
import Codata.Conat
-- Bisimilarity for Conats
import Codata.Conat.Bisimilarity
-- Conat Literals
import Codata.Conat.Literals
-- Properties for Conats
import Codata.Conat.Properties
-- The Covec type and some operations
import Codata.Covec
-- Bisimilarity for Covecs
import Codata.Covec.Bisimilarity
-- A categorical view of Covec
import Codata.Covec.Categorical
-- Typeclass instances for Covec
import Codata.Covec.Instances
-- Properties of operations on the Covec type
import Codata.Covec.Properties
-- The Cowriter type and some operations
import Codata.Cowriter
-- Bisimilarity for Cowriter
import Codata.Cowriter.Bisimilarity
-- The Delay type and some operations
import Codata.Delay
-- Bisimilarity for the Delay type
import Codata.Delay.Bisimilarity
-- A categorical view of Delay
import Codata.Delay.Categorical
-- Properties of operations on the Delay type
import Codata.Delay.Properties
-- M-types (the dual of W-types)
import Codata.M
-- Bisimilarity for M-types
import Codata.M.Bisimilarity
-- Properties of operations on M-types
import Codata.M.Properties
-- "Finite" sets indexed on coinductive "natural" numbers
import Codata.Musical.Cofin
-- Coinductive lists
import Codata.Musical.Colist
-- Coinductive lists: base type and functions
import Codata.Musical.Colist.Base
-- Pointwise equality of colists
import Codata.Musical.Colist.Bisimilarity
-- Infinite merge operation for coinductive lists
import Codata.Musical.Colist.Infinite-merge
-- Properties of coinductive lists and their operations
import Codata.Musical.Colist.Properties
-- Coinductive lists where all elements satisfy a predicate
import Codata.Musical.Colist.Relation.Unary.All
-- Coinductive lists where all elements satisfy a predicate
import Codata.Musical.Colist.Relation.Unary.All.Properties
-- Coinductive lists where at least one element satisfies a predicate
import Codata.Musical.Colist.Relation.Unary.Any
-- Properties of the Any predicate on colists
import Codata.Musical.Colist.Relation.Unary.Any.Properties
-- Coinductive "natural" numbers
import Codata.Musical.Conat
-- Coinductive "natural" numbers: base type and operations
import Codata.Musical.Conat.Base
-- Conversion between coinductive data structures using "musical"
-- coinduction and the ones using sized types.
import Codata.Musical.Conversion
-- Costrings
import Codata.Musical.Costring
-- Coinductive vectors
import Codata.Musical.Covec
-- 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
-- Streams
import Codata.Musical.Stream
-- The Stream type and some operations
import Codata.Stream
-- Bisimilarity for Streams
import Codata.Stream.Bisimilarity
-- A categorical view of Stream
import Codata.Stream.Categorical
-- Typeclass instances for Stream
import Codata.Stream.Instances
-- Properties of operations on the Stream type
import Codata.Stream.Properties
-- The Thunk wrappers for sized codata, copredicates and corelations
import Codata.Thunk
-- 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
-- Sized fixpoints of containers, based on the work of Abbott and others
import Data.Container.Fixpoints.Sized
-- 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
-- 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
-- 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
import Data.Empty
-- An irrelevant version of ⊥-elim
import Data.Empty.Irrelevant
-- Level polymorphic Empty type
import Data.Empty.Polymorphic
-- Wrapper for the erased modality
import Data.Erased
-- 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
-- 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
-- An example of how Data.Fin.Substitution can be used: a definition
-- of substitution for the untyped λ-calculus, along with some lemmas
import Data.Fin.Substitution.Example
-- 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
-- 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
-- Lists
import Data.List
-- Lists, basic types and operations
import Data.List.Base
-- A categorical view of List
import Data.List.Categorical
-- A data structure which keeps track of an upper bound on the number
-- of elements /not/ in a given list
import Data.List.Countdown
-- 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
-- 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
-- Non-empty lists
import Data.List.NonEmpty
-- Non-empty lists: base type and operations
import Data.List.NonEmpty.Base
-- A categorical view of List⁺
import Data.List.NonEmpty.Categorical
-- Typeclass instances for List⁺
import Data.List.NonEmpty.Instances
-- Properties of non-empty lists
import Data.List.NonEmpty.Properties
-- List-related properties
import Data.List.Properties
-- Bag and set equality
import Data.List.Relation.Binary.BagAndSetEquality
-- Pairs of lists that share no common elements (propositional equality)
import Data.List.Relation.Binary.Disjoint.Propositional
-- 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
-- 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
-- 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
-- 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
-- Sublist-related properties
import Data.List.Relation.Binary.Sublist.Propositional.Disjoint
-- 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
-- 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
-- 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
-- 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
-- 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
-- A categorical view of Maybe
import Data.Maybe.Categorical
-- 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
-- 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
-- Primality
import Data.Nat.Primality
-- 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
-- Unsafe operations over linear congruential pseudo random generators
-- for natural numbers
-- /!\ NB: LCGs must not be used for cryptographic applications
import Data.Nat.PseudoRandom.LCG.Unsafe
-- 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
-- Products
import Data.Product
-- Algebraic properties of products
import Data.Product.Algebra
-- Universe-sensitive functor and monad instances for the Product type.
import Data.Product.Categorical.Examples
-- Left-biased universe-sensitive functor and monad instances for the
-- Product type.
import Data.Product.Categorical.Left
-- Base definitions for the left-biased universe-sensitive functor and
-- monad instances for the Product type.
import Data.Product.Categorical.Left.Base
-- Right-biased universe-sensitive functor and monad instances for the
-- Product type.
import Data.Product.Categorical.Right
-- Base definitions for the right-biased universe-sensitive functor
-- and monad instances for the Product type.
import Data.Product.Categorical.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
-- Dependent product combinators for setoid equality preserving
-- functions
import Data.Product.Function.Dependent.Setoid.WithK
-- 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, 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
-- 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 an erased proof.
import Data.Refinement
-- 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
-- Unsafe String operations and proofs
import Data.String.Unsafe
-- 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 categorical view of the Sum type
import Data.Sum.Categorical.Examples
-- A Categorical view of the Sum type (Left-biased)
import Data.Sum.Categorical.Left
-- A Categorical view of the Sum type (Right-biased)
import Data.Sum.Categorical.Right
-- 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.Categorical.Left
-- Base definitions for the left-biased universe-sensitive functor and
-- monad instances for These.
import Data.These.Categorical.Left.Base
-- Right-biased universe-sensitive functor and monad instances for These.
import Data.These.Categorical.Right
-- Base definitions for the right-biased universe-sensitive functor and
-- monad instances for These.
import Data.These.Categorical.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
-- 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
-- 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
-- 1 dimensional pretty printing of binary trees
import Data.Tree.Binary.Show
-- Zippers for Binary Trees
import Data.Tree.Binary.Zipper
-- Tree Zipper-related properties
import Data.Tree.Binary.Zipper.Properties
-- Rose trees
import Data.Tree.Rose
-- Properties of rose trees
import Data.Tree.Rose.Properties
-- 1 dimensional pretty printing of rose trees
import Data.Tree.Rose.Show
-- Trie, basic type and operations
import Data.Trie
-- Non empty trie, basic type and operations
import Data.Trie.NonEmpty
-- The unit type
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
-- A categorical view of Vec
import Data.Vec.Categorical
-- 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
-- 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
-- A categorical view of vectors defined by recursion
import Data.Vec.Recursive.Categorical
-- Properties of n-ary products
import Data.Vec.Recursive.Properties
-- 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 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
-- W-types
import Data.W
-- Indexed W-types aka Petersson-Synek trees
import Data.W.Indexed
-- Sized W-types
import Data.W.Sized
-- Some code related to the W type that relies on the K rule
import Data.W.WithK
-- Machine words
import Data.Word
-- Machine words: basic type and conversion functions
import Data.Word.Base
-- Instances for words
import Data.Word.Instances
-- Properties of operations on machine words
import Data.Word.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
-- Printing Strings During Evaluation
import Debug.Trace
-- This module duplicates `Category.Applicative`
-- for forward compatibility with v2.0.
import Effect.Applicative
-- This module duplicates `Category.Applicative.Indexed`
-- for forward compatibility with v2.0.
import Effect.Applicative.Indexed
-- This module duplicates `Category.Applicative.Predicate`
-- for forward compatibility with v2.0.
import Effect.Applicative.Predicate
-- This module duplicates `Category.Comonad`
-- for forward compatibility with v2.0.
import Effect.Comonad
-- This module duplicates `Category.Functor`
-- for forward compatibility with v2.0.
import Effect.Functor
-- This module duplicates `Category.Functor.Predicate`
-- for forward compatibility with v2.0.
import Effect.Functor.Predicate
-- This module duplicates `Category.Monad`
-- for forward compatibility with v2.0.
import Effect.Monad
-- This module duplicates `Category.Monad.Continuation`
-- for forward compatibility with v2.0.
import Effect.Monad.Continuation
-- This module duplicates `Category.Monad.Indexed`
-- for forward compatibility with v2.0.
import Effect.Monad.Indexed
-- This module duplicates `Category.Monad.Partiality`
-- for forward compatibility with v2.0.
import Effect.Monad.Partiality
-- This module duplicates `Category.Monad.Partiality.All`
-- for forward compatibility with v2.0.
import Effect.Monad.Partiality.All
-- This module duplicates `Category.Monad.Partiality.Instances`
-- for forward compatibility with v2.0.
import Effect.Monad.Partiality.Instances
-- This module duplicates `Category.Monad.Predicate`
-- for forward compatibility with v2.0.
import Effect.Monad.Predicate
-- This module duplicates `Category.Monad.Reader`
-- for forward compatibility with v2.0.
import Effect.Monad.Reader
-- This module duplicates `Category.Monad.State`
-- for forward compatibility with v2.0.
import Effect.Monad.State
-- Type(s) used (only) when calling out to Haskell via the FFI
import Foreign.Haskell
-- Zero-cost coercion to cross the FFI boundary
import Foreign.Haskell.Coerce
-- The Either type which calls out to Haskell via the FFI
import Foreign.Haskell.Either
-- The Pair type which calls out to Haskell via the FFI
import Foreign.Haskell.Pair
-- Functions
import Function
-- Simple combinators working solely on and with functions
import Function.Base
-- Bijections
import Function.Bijection
-- Bundles for types of functions
import Function.Bundles
-- Composition of functional properties
import Function.Construct.Composition
-- The identity function
import Function.Construct.Identity
-- Some functional properties are symmetric
import Function.Construct.Symmetry
-- Definitions for types of functions.
import Function.Definitions
-- Definitions for types of functions that only require an equality
-- relation over the domain.
import Function.Definitions.Core1
-- Definitions for types of functions that only require an equality
-- relation over the co-domain.
import Function.Definitions.Core2
-- Endomorphisms on a Set
import Function.Endomorphism.Propositional
-- Endomorphisms on a Setoid
import Function.Endomorphism.Setoid
-- Function setoids and related constructions
import Function.Equality
-- Equivalence (coinhabitance)
import Function.Equivalence
-- Half adjoint equivalences
import Function.HalfAdjointEquivalence
-- A categorical view of the identity function
import Function.Identity.Categorical
-- Typeclass instances for Identity
import Function.Identity.Instances
-- Injections
import Function.Injection
-- Inverses
import Function.Inverse
-- Left inverses
import Function.LeftInverse
-- 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
-- An Equivalence (on functions) is an Equivalence relation
-- This file is meant to be imported qualified.
import Function.Properties.Equivalence
-- Some functional properties are Equivalence Relations
-- This file is meant to be imported qualified.
import Function.Properties.Inverse
-- A module used for creating function pipelines, see
-- README.Function.Reasoning for examples
import Function.Reasoning
-- A universe which includes several kinds of "relatedness" for sets,
-- such as equivalences, surjections and bijections
import Function.Related
-- 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
-- Structures for types of functions
import Function.Structures
-- Surjections
import Function.Surjection
-- IO
import IO
-- IO: basic types and functions
import IO.Base
-- IO only involving finite objects
import IO.Finite
-- IO only involving infinite objects
import IO.Infinite
-- Primitive IO: simple bindings to Haskell types and functions
import IO.Primitive
-- Primitive IO: simple bindings to Haskell types and functions
-- Everything is assumed to be finite
import IO.Primitive.Finite
-- Primitive IO: simple bindings to Haskell types and functions
-- manipulating potentially infinite objects
import IO.Primitive.Infinite
-- An abstraction of various forms of recursion/induction
import Induction
-- 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
-- Abstractions used in the reflection machinery
import Reflection.Abstraction
-- Annotated reflected syntax.
import Reflection.Annotated
-- Computing free variable annotations on reflected syntax.
import Reflection.Annotated.Free
-- Arguments used in the reflection machinery
import Reflection.Argument
-- Argument information used in the reflection machinery
import Reflection.Argument.Information
-- Modalities used in the reflection machinery
import Reflection.Argument.Modality
-- Argument quantities used in the reflection machinery
import Reflection.Argument.Quantity
-- Argument relevance used in the reflection machinery
import Reflection.Argument.Relevance
-- Argument visibility used in the reflection machinery
import Reflection.Argument.Visibility
-- Weakening, strengthening and free variable check for reflected terms.
import Reflection.DeBruijn
-- Definitions used in the reflection machinery
import Reflection.Definition
-- Support for system calls as part of reflection
import Reflection.External
-- Instances for reflected syntax
import Reflection.Instances
-- Literals used in the reflection machinery
import Reflection.Literal
-- Metavariables used in the reflection machinery
import Reflection.Meta
-- Names used in the reflection machinery
import Reflection.Name
-- Patterns used in the reflection machinery
import Reflection.Pattern
-- Converting reflection machinery to strings
import Reflection.Show
-- Terms used in the reflection machinery
import Reflection.Term
-- de Bruijn-aware generic traversal of reflected terms.
import Reflection.Traversal
-- Printf-style versions of typeError and debugPrint
import Reflection.TypeChecking.Format
-- The TC (Type Checking) monad
import Reflection.TypeChecking.Monad
-- Typeclass instances for TC
import Reflection.TypeChecking.Monad.Categorical
-- Typeclass instances for TC
import Reflection.TypeChecking.Monad.Instances
-- Monad syntax for the TC monad
import Reflection.TypeChecking.Monad.Syntax
-- A universe for the types involved in the reflected syntax.
import Reflection.Universe
-- Properties of homogeneous binary relations
import Relation.Binary
-- Bundles for homogeneous binary relations
import Relation.Binary.Bundles
-- 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` this module does not
-- flip the underlying equality.
import Relation.Binary.Construct.Converse
-- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
-- the module `Relation.Binary.Construct.Converse` this module flips
-- both the relation and the underlying equality.
import Relation.Binary.Construct.Flip
-- 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
-- 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
-- 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
-- Properties satisfied by bounded join semilattices
import Relation.Binary.Properties.BoundedJoinSemilattice
-- Properties satisfied by bounded lattice
import Relation.Binary.Properties.BoundedLattice
-- Properties satisfied by bounded meet semilattices
import Relation.Binary.Properties.BoundedMeetSemilattice
-- Properties satisfied by decidable total orders
import Relation.Binary.Properties.DecTotalOrder
-- Properties for distributive lattice
import Relation.Binary.Properties.DistributiveLattice
-- Properties satisfied by Heyting Algebra
import Relation.Binary.Properties.HeytingAlgebra
-- Properties satisfied by join semilattices
import Relation.Binary.Properties.JoinSemilattice
-- Properties satisfied by lattices
import Relation.Binary.Properties.Lattice
-- Properties satisfied by meet semilattices
import Relation.Binary.Properties.MeetSemilattice
-- 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
-- An equality postulate which evaluates
import Relation.Binary.PropositionalEquality.TrustMe
-- Some code related to propositional equality that relies on the K
-- rule
import Relation.Binary.PropositionalEquality.WithK
-- 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
-- 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
-- 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
-- Implications of nullary relations
import Relation.Nullary.Implication
-- 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
-- Products of nullary relations
import Relation.Nullary.Product
-- Properties of the `Reflects` construct
import Relation.Nullary.Reflects
-- Sums of nullary relations
import Relation.Nullary.Sum
-- A universe of proposition functors, along with some properties
import Relation.Nullary.Universe
-- Unary relations
import Relation.Unary
-- 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
-- Predicate transformers
import Relation.Unary.PredicateTransformer
-- Properties of constructions over unary relations
import Relation.Unary.Properties
-- Indexed unary relations over sized types
import Relation.Unary.Sized
-- Sizes for Agda's sized types
import Size
-- Strictness combinators
import Strict
-- Miscellanous information about the system environment
import System.Environment
-- Primitive System.Environment: simple bindings to Haskell functions
import System.Environment.Primitive
-- Exiting the program.
import System.Exit
-- Primitive System.Exit simple bindings to Haskell functions
import System.Exit.Primitive
-- 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
-- Helper reflection functions
import Tactic.RingSolver.Core.ReflectionHelp
-- 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
-- Pretty Printing
-- This module is based on Jean-Philippe Bernardy's functional pearl
-- "A Pretty But Not Greedy Printer"
import Text.Pretty
-- 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
-- Regular expressions acting on strings, using unsafe features
import Text.Regex.String.Unsafe
-- 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
------------------------------------------------------------------------
-- 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
-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
import Algebra.Bundles
-- Lemmas relating algebraic definitions (such as associativity and
-- commutativity) that don't 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
-- 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
-- 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 ordering.
import Algebra.Construct.NaturalChoice.Base
-- The max operator derived from an arbitrary total order
import Algebra.Construct.NaturalChoice.Max
-- Properties of a max operator derived from a spec over a total order.
import Algebra.Construct.NaturalChoice.MaxOp
-- The min operator derived from an arbitrary total order
import Algebra.Construct.NaturalChoice.Min
-- Properties of min and max operators specified over a total order
import Algebra.Construct.NaturalChoice.MinMaxOp
-- Properties of a min operator derived from a spec over a total order.
import Algebra.Construct.NaturalChoice.MinOp
-- 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.
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 defined over some other
-- structure, like modules and vector spaces
import Algebra.Module.Bundles
-- 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
-- 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 of left-scaling
import Algebra.Module.Definitions.Left
-- Properties of right-scaling
import Algebra.Module.Definitions.Right
-- 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
-- Some properties of Magma homomorphisms
import Algebra.Morphism.Consequences
-- 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 lattice-like structures
import Algebra.Morphism.LatticeMonomorphism
-- 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 derivable properties
import Algebra.Properties.BooleanAlgebra
-- Boolean algebra expressions
import Algebra.Properties.BooleanAlgebra.Expression
-- 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
-- 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.DistributiveLattice
-- Some derivable properties
import Algebra.Properties.Group
-- Some derivable properties
import Algebra.Properties.Lattice
-- Divisibility over magmas
import Algebra.Properties.Magma.Divisibility
-- 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 basic properties of Rings
import Algebra.Properties.Ring
-- Some theory for Semigroup
import Algebra.Properties.Semigroup
-- Properties of divisibility over semigroups
import Algebra.Properties.Semigroup.Divisibility
-- Some derivable properties
import Algebra.Properties.Semilattice
-- 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
-- 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
-- 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
-- A solver for equations over monoids
import Algebra.Solver.Monoid
-- 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
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
-- Applicative functors
import Category.Applicative
-- Indexed applicative functors
import Category.Applicative.Indexed
-- Applicative functors on indexed sets (predicates)
import Category.Applicative.Predicate
-- Comonads
import Category.Comonad
-- Functors
import Category.Functor
-- Functors on indexed sets (predicates)
import Category.Functor.Predicate
-- Monads
import Category.Monad
-- A delimited continuation monad
import Category.Monad.Continuation
-- Indexed monads
import Category.Monad.Indexed
-- The partiality monad
import Category.Monad.Partiality
-- An All predicate for the partiality monad
import Category.Monad.Partiality.All
-- Typeclass instances for _⊥
import Category.Monad.Partiality.Instances
-- Monads on indexed sets (predicates)
import Category.Monad.Predicate
-- The reader monad
import Category.Monad.Reader
-- The state monad
import Category.Monad.State
-- "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
-- 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
-- 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
import Data.Empty
-- An irrelevant version of ⊥-elim
import Data.Empty.Irrelevant
-- Level polymorphic Empty type
import Data.Empty.Polymorphic
-- Wrapper for the erased modality
import Data.Erased
-- 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
-- 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
-- An example of how Data.Fin.Substitution can be used: a definition
-- of substitution for the untyped λ-calculus, along with some lemmas