Created
November 29, 2023 15:02
-
-
Save andy0130tw/f964b5a95c45204e3a99b8378de24d75 to your computer and use it in GitHub Desktop.
agda-stdlib's Everything v1.7.3
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
------------------------------------------------------------------------ | |
-- 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 | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
------------------------------------------------------------------------ | |
-- 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 | |
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 | |
-- 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 | |
-- 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 | |
-- Zippers for Binary Trees | |
import Data.Tree.Binary.Zipper | |
-- Tree Zipper-related properties | |
import Data.Tree.Binary.Zipper.Properties | |
-- 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 | |
-- 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 | |
-- 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 | |
-- 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 | |
-- 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 | |
-- 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 | |
-- Strictness combinators | |
import Strict | |
-- 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 | |
-- Printf | |
import Text.Printf | |
-- Generic printf function. | |
import Text.Printf.Generic | |
-- Regular expressions | |
import Text.Regex | |
-- Regular expressions: basic types and semantics | |
import Text.Regex.Base | |
-- Regular expressions: Brzozowski derivative | |
import Text.Regex.Derivative.Brzozowski | |
-- Properties of regular expressions and their semantics | |
import Text.Regex.Properties | |
-- Regular expressions: search algorithms | |
import Text.Regex.Search | |
-- Regular expressions: smart constructors | |
-- Computing the Brzozowski derivative of a regular expression may lead | |
-- to a blow-up in the size of the expression. To keep it tractable it | |
-- is crucial to use smart constructors. | |
import Text.Regex.SmartConstructors | |
-- Regular expressions acting on strings | |
import Text.Regex.String | |
-- Fancy display functions for List-based tables | |
import Text.Tabular.Base | |
-- Fancy display functions for List-based tables | |
import Text.Tabular.List | |
-- Fancy display functions for Vec-based tables | |
import Text.Tabular.Vec | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment