Agda

• Agda.Benchmarking9Agda-specific benchmarking structure.
• Agda.Compiler.Backend1611Interface for compiler backend writers.
• Agda.Compiler.Backend.Base3
• Agda.Compiler.Builtin1Built-in backends.
• Agda.Compiler.CallCompiler2A command which calls a compiler
• Agda.Compiler.Common12
• Agda.Compiler.JS.Compiler42Main module for JS backend.
• Agda.Compiler.JS.Pretty31
• Agda.Compiler.JS.Substitution18
• Agda.Compiler.JS.Syntax10
• Agda.Compiler.MAlonzo.Coerce2
• Agda.Compiler.MAlonzo.Compiler2
• Agda.Compiler.MAlonzo.Encode1
• Agda.Compiler.MAlonzo.HaskellTypes4Translating Agda types to Haskell types. Used to ensure that imported
• Agda.Compiler.MAlonzo.Misc66
• Agda.Compiler.MAlonzo.Pragmas13
• Agda.Compiler.MAlonzo.Pretty6
• Agda.Compiler.MAlonzo.Primitives11
• Agda.Compiler.MAlonzo.Strict1Strictification of Haskell code
• Agda.Compiler.ToTreeless6
• Agda.Compiler.Treeless.AsPatterns1
• Agda.Compiler.Treeless.Builtin1Translates the Agda builtin nat datatype to arbitrary-precision integers. Philipp, 20150921:
• Agda.Compiler.Treeless.Compare1
• Agda.Compiler.Treeless.EliminateDefaults1Eliminates case defaults by adding an alternative for all possible
• Agda.Compiler.Treeless.EliminateLiteralPatterns3Converts case matches on literals to if cascades with equality comparisons.
• Agda.Compiler.Treeless.Erase3
• Agda.Compiler.Treeless.GuardsToPrims1Translates guard alternatives to if-then-else cascades. The builtin translation must be run before this transformation.
• Agda.Compiler.Treeless.Identity1
• Agda.Compiler.Treeless.NormalizeNames1Ensures that all occurences of an abstract name share
• Agda.Compiler.Treeless.Pretty0
• Agda.Compiler.Treeless.Simplify1
• Agda.Compiler.Treeless.Subst12
• Agda.Compiler.Treeless.Uncase1
• Agda.Compiler.Treeless.Unused2
• Agda.ImpossibleTest2Facility to test throwing internal errors.
• Agda.Interaction.AgdaTop1
• Agda.Interaction.Base27
• Agda.Interaction.BasicOps48
• Agda.Interaction.CommandLine1
• Agda.Interaction.EmacsCommand7Code for instructing Emacs to do things
• Agda.Interaction.EmacsTop7
• Agda.Interaction.ExitCode5
• Agda.Interaction.FindFile16Functions which map between module names and file names. Note that file name lookups are cached in the TCState. The code
• Agda.Interaction.Highlighting.Common2Common syntax highlighting functions for Emacs and JSON
• Agda.Interaction.Highlighting.Dot1
• Agda.Interaction.Highlighting.Emacs2Functions which give precise syntax highlighting info to Emacs.
• Agda.Interaction.Highlighting.FromAbstract2Extract highlighting syntax from abstract syntax. Implements one big fold over abstract syntax.
• Agda.Interaction.Highlighting.Generate17Generates data used for precise syntax highlighting.
• Agda.Interaction.Highlighting.HTML1Backend for generating highlighted, hyperlinked HTML from Agda sources.
• Agda.Interaction.Highlighting.JSON1Functions which give precise syntax highlighting info in JSON format.
• Agda.Interaction.Highlighting.LaTeX1Generating highlighted and aligned LaTeX from literate Agda source.
• Agda.Interaction.Highlighting.Precise22Types used for precise syntax highlighting.
• Agda.Interaction.Highlighting.Range12Ranges.
• Agda.Interaction.Highlighting.Vim8
• Agda.Interaction.Imports15This module deals with finding imported modules and loading their
• Agda.Interaction.InteractionTop45
• Agda.Interaction.JSON115Encoding stuff into JSON values in TCM
• Agda.Interaction.JSONTop1
• Agda.Interaction.Library22Library management. Sample use: -- Get libraries as listed in .agda/libraries file.
• Agda.Interaction.Library.Base41Basic data types for library management.
• Agda.Interaction.Library.Parse4Parser for .agda-lib files. Example file: name: Main
• Agda.Interaction.MakeCase11
• Agda.Interaction.Monad3
• Agda.Interaction.Options177
• Agda.Interaction.Options.Help4
• Agda.Interaction.Options.Lenses27Lenses for CommandLineOptions and PragmaOptions. Add as needed. Nothing smart happening here.
• Agda.Interaction.Options.Warnings21
• Agda.Interaction.Output2
• Agda.Interaction.Response8
• Agda.Interaction.Response.Base11Data type for all interactive responses
• Agda.Interaction.SearchAbout1
• Agda.Main20Agda main module.
• Agda.Mimer.Mimer2
• Agda.Mimer.Options9
• Agda.Syntax.Abstract82The abstract syntax. This is what you get after desugaring and scope
• Agda.Syntax.Abstract.Name47Abstract names carry unique identifiers and stuff.
• Agda.Syntax.Abstract.Pattern30Auxiliary functions to handle patterns in the abstract syntax. Generic and specific traversals.
• Agda.Syntax.Abstract.PatternSynonyms3Pattern synonym utilities: folding pattern synonym definitions for
• Agda.Syntax.Abstract.Pretty5
• Agda.Syntax.Abstract.UsedNames1
• Agda.Syntax.Abstract.Views25
• Agda.Syntax.Builtin232This module defines the names of all builtin and primitives used in Agda. See Agda.TypeChecking.Monad.Builtin
• Agda.Syntax.Common260Some common syntactic entities are defined in this module.
• Agda.Syntax.Common.Aspect7
• Agda.Syntax.Common.KeywordRange2A abstract Range type dedicated to keyword occurrences in the source.
• Agda.Syntax.Common.Pretty81Pretty printing functions.
• Agda.Syntax.Common.Pretty.ANSI2
• Agda.Syntax.Concrete83The concrete syntax is a raw representation of the program text
• Agda.Syntax.Concrete.Attribute24
• Agda.Syntax.Concrete.Definitions16Preprocess Declarations, producing NiceDeclarations. Attach fixity and syntax declarations to the definition they refer to. Distribute t…
• Agda.Syntax.Concrete.Definitions.Errors9
• Agda.Syntax.Concrete.Definitions.Monad36
• Agda.Syntax.Concrete.Definitions.Types27
• Agda.Syntax.Concrete.Fixity5Collecting fixity declarations (and polarity pragmas) for concrete
• Agda.Syntax.Concrete.Generic3Generic traversal and reduce for concrete syntax,
• Agda.Syntax.Concrete.Glyph12Choice of Unicode or ASCII glyphs.
• Agda.Syntax.Concrete.Name41Names in the concrete syntax are just strings (or lists of strings for
• Agda.Syntax.Concrete.Operators5The parser doesn't know about operators and parses everything as normal
• Agda.Syntax.Concrete.Operators.Parser16
• Agda.Syntax.Concrete.Operators.Parser.Monad10The parser monad used by the operator parser
• Agda.Syntax.Concrete.Pattern25Tools for patterns in concrete syntax.
• Agda.Syntax.Concrete.Pretty19Pretty printer for the concrete syntax.
• Agda.Syntax.DoNotation1Desugaring for do-notation. Uses whatever `_>>=_` and `_>>_` happen to be
• Agda.Syntax.Fixity17Definitions for fixity, precedence levels, and declared syntax.
• Agda.Syntax.IdiomBrackets1
• Agda.Syntax.Info22An info object contains additional information about a piece of abstract
• Agda.Syntax.Literal4
• Agda.Syntax.Notation19As a concrete name, a notation is a non-empty list of alternating IdParts and holes.
• Agda.Syntax.Parser16
• Agda.Syntax.Parser.Alex15This module defines the things required by Alex and some other
• Agda.Syntax.Parser.Comments5This module defines the lex action to lex nested comments. As is well-known
• Agda.Syntax.Parser.Helpers52Utility functions used in the Happy parser.
• Agda.Syntax.Parser.Layout5This module contains the lex actions that handle the layout rules. The way
• Agda.Syntax.Parser.LexActions24This module contains the building blocks used to construct the lexer.
• Agda.Syntax.Parser.Lexer9The lexer is generated by Alex (http://www.haskell.org/alex) and is an
• Agda.Syntax.Parser.Literate15Preprocessors for literate code formats.
• Agda.Syntax.Parser.LookAhead12When lexing by hand (for instance string literals) we need to do some
• Agda.Syntax.Parser.Monad38
• Agda.Syntax.Parser.Parser6The parser is generated by Happy (http://www.haskell.org/happy).
• Agda.Syntax.Parser.StringLiterals2The code to lex string and character literals. Basically the same code
• Agda.Syntax.Parser.Tokens4
• Agda.Syntax.Position56Position information for syntax. Crucial for giving good error messages.
• Agda.Syntax.Reflected12
• Agda.Syntax.Scope.Base132This module defines the notion of a scope and operations on scopes.
• Agda.Syntax.Scope.Flat4Flattened scopes.
• Agda.Syntax.Scope.Monad73The scope monad with operations.
• Agda.Syntax.TopLevelModuleName13
• Agda.Syntax.TopLevelModuleName.Boot4
• Agda.Syntax.Translation.AbstractToConcrete15The translation of abstract syntax to concrete syntax has two purposes.
• Agda.Syntax.Translation.ConcreteToAbstract17Translation from Agda.Syntax.Concrete to Agda.Syntax.Abstract.
• Agda.Syntax.Translation.InternalToAbstract7Translating from internal syntax to abstract syntax. Enables nice
• Agda.Syntax.Translation.ReflectedToAbstract18
• Agda.Syntax.Treeless33The treeless syntax is intended to be used as input for the compiler backends.
• Agda.Termination.CallGraph16Call graphs and related concepts, more or less as defined in
• Agda.Termination.CallMatrix10
• Agda.Termination.CutOff2Defines CutOff type which is used in Agda.Interaction.Options.
• Agda.Termination.Monad54The monad for the termination checker. The termination monad TerM is an extension of
• Agda.Termination.Order19An Abstract domain of relative sizes, i.e., differences
• Agda.Termination.RecCheck3Checking for recursion: We detect truly (co)recursive definitions by computing the
• Agda.Termination.Semiring5Semirings.
• Agda.Termination.SparseMatrix23Sparse matrices. We assume the matrices to be very sparse, so we just implement them as
• Agda.Termination.TermCheck3
• Agda.Termination.Termination4Termination checker, based on
• Agda.TheTypeChecker5
• Agda.TypeChecking.Abstract8Functions for abstracting terms over other terms.
• Agda.TypeChecking.CheckInternal8A bidirectional type checker for internal syntax. Performs checking on unreduced terms.
• Agda.TypeChecking.CompiledClause13Case trees. After coverage checking, pattern matching is translated
• Agda.TypeChecking.CompiledClause.Compile16
• Agda.TypeChecking.CompiledClause.Match5
• Agda.TypeChecking.Constraints24
• Agda.TypeChecking.Conversion50
• Agda.TypeChecking.Conversion.Pure6
• Agda.TypeChecking.Coverage11Coverage checking, case splitting, and splitting for refine tactics.
• Agda.TypeChecking.Coverage.Cubical7
• Agda.TypeChecking.Coverage.Match16Given the function clauses cs the patterns ps of the split clause we want to compute a variable index (in the split clause) to split on …
• Agda.TypeChecking.Coverage.SplitClause7SplitClause and CoverResult types.
• Agda.TypeChecking.Coverage.SplitTree9Split tree for transforming pattern clauses into case trees. The coverage checker generates a split tree from the clauses.
• Agda.TypeChecking.Datatypes23
• Agda.TypeChecking.DeadCode1
• Agda.TypeChecking.DiscrimTree5Imperfect discrimination trees for indexing data by internal
• Agda.TypeChecking.DiscrimTree.Types4
• Agda.TypeChecking.DisplayForm1Tools for DisplayTerm and DisplayForm.
• Agda.TypeChecking.DropArgs1
• Agda.TypeChecking.Empty4
• Agda.TypeChecking.Errors17
• Agda.TypeChecking.EtaContract6Compute eta short normal forms.
• Agda.TypeChecking.Forcing3A constructor argument is forced if it appears as pattern variable
• Agda.TypeChecking.Free39Computing the free variables of a term. The distinction between rigid and strongly rigid occurrences comes from:
• Agda.TypeChecking.Free.Lazy51Computing the free variables of a term lazily. We implement a reduce (traversal into monoid) over internal syntax
• Agda.TypeChecking.Free.Precompute4Precompute free variables in a term (and store in ArgInfo).
• Agda.TypeChecking.Free.Reduce4Free variable check that reduces the subject to make certain variables not
• Agda.TypeChecking.Functions2
• Agda.TypeChecking.Generalize3This module implements the type checking part of generalisable variables. When we get here we have
• Agda.TypeChecking.IApplyConfluence4
• Agda.TypeChecking.Implicit10Functions for inserting implicit arguments at the right places.
• Agda.TypeChecking.Injectivity15Injectivity, or more precisely, "constructor headedness", is a
• Agda.TypeChecking.Inlining1Logic for deciding which functions should be automatically inlined.
• Agda.TypeChecking.InstanceArguments13
• Agda.TypeChecking.Irrelevance10Compile-time irrelevance. In type theory with compile-time irrelevance à la Pfenning (LiCS 2001),
• Agda.TypeChecking.Level26
• Agda.TypeChecking.Level.Solve2
• Agda.TypeChecking.LevelConstraints1
• Agda.TypeChecking.Lock3
• Agda.TypeChecking.MetaVars66
• Agda.TypeChecking.MetaVars.Mention2
• Agda.TypeChecking.MetaVars.Occurs38The occurs check for unification. Does pruning on the fly. When hitting a meta variable: Compute flex/rigid for its arguments. Compare …
• Agda.TypeChecking.Modalities3
• Agda.TypeChecking.Monad0
• Agda.TypeChecking.Monad.Base562
• Agda.TypeChecking.Monad.Base.Types2Data structures for the type checker. Part of Agda.TypeChecking.Monad.Base, extracted to avoid import cycles.
• Agda.TypeChecking.Monad.Base.Warning1Types related to warnings raised by Agda.
• Agda.TypeChecking.Monad.Benchmark9Measure CPU time for individual phases of the Agda pipeline.
• Agda.TypeChecking.Monad.Builtin264
• Agda.TypeChecking.Monad.Caching10
• Agda.TypeChecking.Monad.Closure3
• Agda.TypeChecking.Monad.Constraints34
• Agda.TypeChecking.Monad.Context43
• Agda.TypeChecking.Monad.Debug32
• Agda.TypeChecking.Monad.Env26
• Agda.TypeChecking.Monad.Imports15
• Agda.TypeChecking.Monad.MetaVars79
• Agda.TypeChecking.Monad.Modality16Modality. Agda has support for several modalities, namely: Cohesion Quantity Relevance In order to type check such modalities, we must …
• Agda.TypeChecking.Monad.Mutual8
• Agda.TypeChecking.Monad.Open4
• Agda.TypeChecking.Monad.Options39
• Agda.TypeChecking.Monad.Pure1A typeclass collecting all pure typechecking operations
• Agda.TypeChecking.Monad.Signature98
• Agda.TypeChecking.Monad.SizedTypes40Stuff for sized types that does not require modules
• Agda.TypeChecking.Monad.State75Lenses for TCState and more.
• Agda.TypeChecking.Monad.Statistics7Collect statistics.
• Agda.TypeChecking.Monad.Trace5
• Agda.TypeChecking.Names32EDSL to construct terms without touching De Bruijn indices. e.g. given t, u :: Term, Γ ⊢ t, u : A, we can build "λ f. f t u" like this: r…
• Agda.TypeChecking.Opacity3
• Agda.TypeChecking.Patterns.Abstract3Tools to manipulate patterns in abstract syntax
• Agda.TypeChecking.Patterns.Match16Pattern matcher used in the reducer for clauses that
• Agda.TypeChecking.Polarity5Computing the polarity (variance) of function arguments,
• Agda.TypeChecking.Positivity22Check that a datatype is strictly positive.
• Agda.TypeChecking.Positivity.Occurrence5Occurrences.
• Agda.TypeChecking.Pretty46
• Agda.TypeChecking.Pretty.Call2
• Agda.TypeChecking.Pretty.Constraint4
• Agda.TypeChecking.Pretty.Warning18
• Agda.TypeChecking.Primitive39Primitive functions, such as addition on builtin integers.
• Agda.TypeChecking.Primitive.Base44
• Agda.TypeChecking.Primitive.Cubical40
• Agda.TypeChecking.Primitive.Cubical.Base24Implementations of the basic primitives of Cubical Agda: The
• Agda.TypeChecking.Primitive.Cubical.Glue5
• Agda.TypeChecking.Primitive.Cubical.HCompU3
• Agda.TypeChecking.Primitive.Cubical.Id5Implementation of the primitives relating to Cubical identity types.
• Agda.TypeChecking.ProjectionLike10Dropping initial arguments (`parameters') from a function which can be
• Agda.TypeChecking.Quote13
• Agda.TypeChecking.ReconstructParameters11Reconstruct dropped parameters from constructors. Used by
• Agda.TypeChecking.RecordPatterns5Code which replaces pattern matching on record constructors with
• Agda.TypeChecking.Records59
• Agda.TypeChecking.Reduce39
• Agda.TypeChecking.Reduce.Fast2This module implements the Agda Abstract Machine used for compile-time reduction. It's a
• Agda.TypeChecking.Reduce.Monad5
• Agda.TypeChecking.Rewriting9Rewriting with arbitrary rules. The user specifies a relation symbol by the pragma
• Agda.TypeChecking.Rewriting.Clause4
• Agda.TypeChecking.Rewriting.Confluence3Checking local or global confluence of rewrite rules. For checking LOCAL CONFLUENCE of a given rewrite rule f ps ↦ v,
• Agda.TypeChecking.Rewriting.NonLinMatch18Non-linear matching of the lhs of a rewrite rule against a
• Agda.TypeChecking.Rewriting.NonLinPattern13Various utility functions dealing with the non-linear, higher-order
• Agda.TypeChecking.Rules.Application7
• Agda.TypeChecking.Rules.Builtin6
• Agda.TypeChecking.Rules.Builtin.Coinduction6Handling of the INFINITY, SHARP and FLAT builtins.
• Agda.TypeChecking.Rules.Data22
• Agda.TypeChecking.Rules.Decl34
• Agda.TypeChecking.Rules.Def24
• Agda.TypeChecking.Rules.Display1
• Agda.TypeChecking.Rules.LHS6
• Agda.TypeChecking.Rules.LHS.Implicit4
• Agda.TypeChecking.Rules.LHS.Problem24
• Agda.TypeChecking.Rules.LHS.ProblemRest6
• Agda.TypeChecking.Rules.LHS.Unify5Unification algorithm for specializing datatype indices, as described in
• Agda.TypeChecking.Rules.LHS.Unify.LeftInverse7
• Agda.TypeChecking.Rules.LHS.Unify.Types31
• Agda.TypeChecking.Rules.Record5
• Agda.TypeChecking.Rules.Term58
• Agda.TypeChecking.Serialise8Structure-sharing serialisation of Agda interface files.
• Agda.TypeChecking.Serialise.Base33
• Agda.TypeChecking.Serialise.Instances0
• Agda.TypeChecking.Serialise.Instances.Abstract3
• Agda.TypeChecking.Serialise.Instances.Common1
• Agda.TypeChecking.Serialise.Instances.Compilers0
• Agda.TypeChecking.Serialise.Instances.Errors0
• Agda.TypeChecking.Serialise.Instances.Highlighting0
• Agda.TypeChecking.SizedTypes30
• Agda.TypeChecking.SizedTypes.Pretty1
• Agda.TypeChecking.SizedTypes.Solve10Solving size constraints under hypotheses. The size solver proceeds as follows: Get size constraints, cluster into connected components. …
• Agda.TypeChecking.SizedTypes.Syntax30Syntax of size expressions and constraints.
• Agda.TypeChecking.SizedTypes.Utils8
• Agda.TypeChecking.SizedTypes.WarshallSolver72
• Agda.TypeChecking.Sort12This module contains the rules for Agda's sort system viewed as a pure
• Agda.TypeChecking.Substitute64This module contains the definition of hereditary substitution
• Agda.TypeChecking.Substitute.Class39
• Agda.TypeChecking.Substitute.DeBruijn1
• Agda.TypeChecking.SyntacticEquality4A syntactic equality check that takes meta instantiations into account,
• Agda.TypeChecking.Telescope64
• Agda.TypeChecking.Telescope.Path5
• Agda.TypeChecking.Unquote38
• Agda.TypeChecking.Warnings19
• Agda.TypeChecking.With8
• Agda.Utils.AffineHole1Contexts with at most one hole.
• Agda.Utils.Applicative5
• Agda.Utils.AssocList11Additional functions for association lists.
• Agda.Utils.Bag20A simple overlay over Data.Map to manage unordered sets with duplicates.
• Agda.Utils.Benchmark18Tools for benchmarking and accumulating results.
• Agda.Utils.BiMap34Partly invertible finite maps. Time complexities are given under the assumption that all relevant
• Agda.Utils.BoolSet24Representation of Set Bool as a 4-element enum type. All operations in constant time and space. Mimics the interface of Data.Set. Import as:
• Agda.Utils.Boolean2Boolean algebras and types isomorphic to Bool. There are already solutions for Boolean algebras in the Haskell ecosystem,
• Agda.Utils.CallStack25
• Agda.Utils.Char4Agda strings uses Data.Text [1], which can only represent unicode scalar values [2], excluding
• Agda.Utils.Cluster4Create clusters of non-overlapping things.
• Agda.Utils.Either18Utilities for the Either type.
• Agda.Utils.Empty3An empty type with some useful instances.
• Agda.Utils.Environment3Expand environment variables in strings
• Agda.Utils.Fail2A pure MonadFail.
• Agda.Utils.Favorites9Maintaining a list of favorites of some partially ordered type.
• Agda.Utils.FileName9Operations on file names.
• Agda.Utils.Float43Logically consistent comparison of floating point numbers.
• Agda.Utils.Function17
• Agda.Utils.Functor8Utilities for functors.
• Agda.Utils.Graph.AdjacencyMap.Unidirectional66Directed graphs (can of course simulate undirected graphs). Represented as adjacency maps in direction from source to target. Each source…
• Agda.Utils.Graph.TopSort1
• Agda.Utils.Hash6Instead of checking time-stamps we compute a hash of the module source and
• Agda.Utils.HashTable6Hash tables.
• Agda.Utils.Haskell.Syntax25ASTs for subset of GHC Haskell syntax.
• Agda.Utils.IArray24Array utilities.
• Agda.Utils.IO2Auxiliary functions for the IO monad.
• Agda.Utils.IO.Binary1Binary IO.
• Agda.Utils.IO.Directory2
• Agda.Utils.IO.TempFile1Common syntax highlighting functions for Emacs and JSON
• Agda.Utils.IO.UTF85Text IO using the UTF8 character encoding.
• Agda.Utils.IORef11Utilities for Data.IORef.
• Agda.Utils.Impossible6An interface for reporting "impossible" errors
• Agda.Utils.IndexedList11
• Agda.Utils.IntSet.Infinite10Possibly infinite sets of integers (but with finitely many consecutive
• Agda.Utils.Lens23A cut-down implementation of lenses, with names taken from
• Agda.Utils.Lens.Examples3Examples how to use Agda.Utils.Lens.
• Agda.Utils.List74Utility functions for lists.
• Agda.Utils.List1103Non-empty lists. Better name List1 for non-empty lists, plus missing functionality. Import:
• Agda.Utils.List215Lists of length at least 2. Import as:
• Agda.Utils.ListT18ListT done right,
• Agda.Utils.Map3
• Agda.Utils.Maybe29Extend Maybe by common operations for the Maybe type. Note: since this module is usually imported unqualified,
• Agda.Utils.Maybe.Strict22A strict version of the Maybe type. Import qualified, as in
• Agda.Utils.Memo4
• Agda.Utils.Monad47
• Agda.Utils.Monoid1More monoids.
• Agda.Utils.Null10Overloaded null and empty for collections and sequences.
• Agda.Utils.POMonoid4Partially ordered monoids.
• Agda.Utils.Parser.MemoisedCPS13Parser combinators with support for left recursion, following
• Agda.Utils.PartialOrd14
• Agda.Utils.Permutation17
• Agda.Utils.Pointer6
• Agda.Utils.ProfileOptions8
• Agda.Utils.RangeMap10Maps containing non-overlapping intervals.
• Agda.Utils.SemiRing2
• Agda.Utils.Semigroup1Some semigroup instances used in several places
• Agda.Utils.Singleton3Constructing singleton collections.
• Agda.Utils.Size4Collection size. For TermSize see Agda.Syntax.Internal.
• Agda.Utils.SmallSet22Small sets represented as a bitmask for fast membership checking. With the exception of converting to/from lists, all operations are O(1)…
• Agda.Utils.String10
• Agda.Utils.Suffix8
• Agda.Utils.Three6Tools for 3-way partitioning.
• Agda.Utils.Time6Time-related utilities.
• Agda.Utils.Trie20Strict tries (based on Data.Map.Strict and Agda.Utils.Maybe.Strict).
• Agda.Utils.Tuple14
• Agda.Utils.TypeLevel25
• Agda.Utils.TypeLits4Type level literals, inspired by GHC.TypeLits.
• Agda.Utils.Unsafe1
• Agda.Utils.Update15
• Agda.Utils.VarSet15Var field implementation of sets of (small) natural numbers.
• Agda.Utils.Warshall33Construct a graph from constraints
• Agda.Utils.WithDefault7Potentially uninitialised Booleans. The motivation for this small library is to distinguish
• Agda.Utils.Zipper3
• Agda.Version3
• Agda.VersionCommit2

• STMonadTrans-0.4.8in this set
• aeson-2.2.3.0in this set
• ansi-terminal-1.1.3in this set
• array-0.5.8.0with GHC
• async-2.2.5in this set
• base-4.20.2.0with GHC
• binary-0.8.9.3with GHC
• blaze-html-0.9.2.0in this set
• boxes-0.1.5in this set
• bytestring-0.12.2.0with GHC
• case-insensitive-1.2.1.0in this set
• containers-0.7with GHC
• data-hash-0.2.0.1in this set
• deepseq-1.5.0.0with GHC
• directory-1.3.8.5with GHC
• dlist-1.0in this set
• edit-distance-0.2.2.1in this set
• equivalence-0.4.1in this set
• exceptions-0.10.9with GHC
• filepath-1.5.4.0with GHC
• ghc-compact-0.1.0.0with GHC
• gitrev-1.3.1in this set
• hashable-1.4.7.0in this set
• haskeline-0.8.2.1with GHC
• monad-control-1.0.3.1in this set
• mtl-2.3.1with GHC
• murmur-hash-0.1.0.11in this set
• parallel-3.2.2.0in this set
• peano-0.1.0.2in this set
• pqueue-1.5.0.0in this set
• pretty-1.1.3.6with GHC
• process-1.6.26.1with GHC
• regex-tdfa-1.3.2.5in this set
• split-0.2.5in this set
• stm-2.5.3.1with GHC
• strict-0.5.1in this set
• text-2.1.3with GHC
• time-1.12.2with GHC
• transformers-0.6.1.1with GHC
• unordered-containers-0.2.21in this set
• uri-encode-1.5.0.7in this set
• vector-0.13.2.0in this set
• vector-hashtables-0.1.2.0in this set
• zlib-0.7.1.0in this set

Used by in this set · 0

Nothing in this set depends on it.