Agda

• Agda.BenchmarkingAgda-specific benchmarking structure.
• Agda.Compiler.BackendInterface for compiler backend writers.
• Agda.Compiler.Backend.Base
• Agda.Compiler.BuiltinBuilt-in backends.
• Agda.Compiler.CallCompilerA command which calls a compiler
• Agda.Compiler.Common
• Agda.Compiler.JS.CompilerMain module for JS backend.
• Agda.Compiler.JS.Pretty
• Agda.Compiler.JS.Substitution
• Agda.Compiler.JS.Syntax
• Agda.Compiler.MAlonzo.Coerce
• Agda.Compiler.MAlonzo.Compiler
• Agda.Compiler.MAlonzo.Encode
• Agda.Compiler.MAlonzo.HaskellTypesTranslating Agda types to Haskell types. Used to ensure that imported
• Agda.Compiler.MAlonzo.Misc
• Agda.Compiler.MAlonzo.Pragmas
• Agda.Compiler.MAlonzo.Pretty
• Agda.Compiler.MAlonzo.Primitives
• Agda.Compiler.MAlonzo.StrictStrictification of Haskell code
• Agda.Compiler.ToTreeless
• Agda.Compiler.Treeless.AsPatterns
• Agda.Compiler.Treeless.BuiltinTranslates the Agda builtin nat datatype to arbitrary-precision integers. Philipp, 20150921:
• Agda.Compiler.Treeless.Compare
• Agda.Compiler.Treeless.EliminateDefaultsEliminates case defaults by adding an alternative for all possible
• Agda.Compiler.Treeless.EliminateLiteralPatternsConverts case matches on literals to if cascades with equality comparisons.
• Agda.Compiler.Treeless.Erase
• Agda.Compiler.Treeless.GuardsToPrimsTranslates guard alternatives to if-then-else cascades. The builtin translation must be run before this transformation.
• Agda.Compiler.Treeless.Identity
• Agda.Compiler.Treeless.NormalizeNamesEnsures that all occurences of an abstract name share
• Agda.Compiler.Treeless.Pretty
• Agda.Compiler.Treeless.Simplify
• Agda.Compiler.Treeless.Subst
• Agda.Compiler.Treeless.Uncase
• Agda.Compiler.Treeless.Unused
• Agda.ImpossibleTestFacility to test throwing internal errors.
• Agda.Interaction.AgdaTop
• Agda.Interaction.Base
• Agda.Interaction.BasicOps
• Agda.Interaction.BuildLibraryType-check all files of a library (option --build-library).
• Agda.Interaction.Command
• Agda.Interaction.CommandLine
• Agda.Interaction.EmacsCommandCode for instructing Emacs to do things
• Agda.Interaction.EmacsTop
• Agda.Interaction.ExitCode
• Agda.Interaction.FindFileFunctions which map between module names and file names. Note that file name lookups are cached in the TCState. The code
• Agda.Interaction.Highlighting.CommonCommon syntax highlighting functions for Emacs and JSON
• Agda.Interaction.Highlighting.Dot
• Agda.Interaction.Highlighting.Dot.Backend
• Agda.Interaction.Highlighting.Dot.BaseGenerate an import dependency graph for a given module.
• Agda.Interaction.Highlighting.EmacsFunctions which give precise syntax highlighting info to Emacs.
• Agda.Interaction.Highlighting.FromAbstractExtract highlighting syntax from abstract syntax. Implements one big fold over abstract syntax.
• Agda.Interaction.Highlighting.GenerateGenerates data used for precise syntax highlighting.
• Agda.Interaction.Highlighting.HTMLBackend for generating highlighted, hyperlinked HTML from Agda sources.
• Agda.Interaction.Highlighting.HTML.BackendBackend for generating highlighted, hyperlinked HTML from Agda sources.
• Agda.Interaction.Highlighting.HTML.BaseFunction for generating highlighted, hyperlinked HTML from Agda
• Agda.Interaction.Highlighting.JSONFunctions which give precise syntax highlighting info in JSON format.
• Agda.Interaction.Highlighting.LaTeXGenerating highlighted and aligned LaTeX from literate Agda source.
• Agda.Interaction.Highlighting.LaTeX.Backend
• Agda.Interaction.Highlighting.LaTeX.BaseFunction for generating highlighted and aligned LaTeX from literate
• Agda.Interaction.Highlighting.PreciseTypes used for precise syntax highlighting.
• Agda.Interaction.Highlighting.RangeRanges.
• Agda.Interaction.Highlighting.Vim
• Agda.Interaction.ImportsThis module deals with finding imported modules and loading their
• Agda.Interaction.InteractionTop
• Agda.Interaction.JSONEncoding stuff into JSON values in TCM
• Agda.Interaction.JSONTop
• Agda.Interaction.LibraryLibrary management. Sample use: -- Get libraries as listed in .agda/libraries file.
• Agda.Interaction.Library.BaseBasic data types for library management.
• Agda.Interaction.Library.ParseParser for .agda-lib files. Example file: name: Main
• Agda.Interaction.MakeCase
• Agda.Interaction.Monad
• Agda.Interaction.Options
• Agda.Interaction.Options.ErrorsProvide names for the errors Agda throws.Options/Er
• Agda.Interaction.Options.Help
• Agda.Interaction.Options.LensesLenses for CommandLineOptions and PragmaOptions. Add as needed. Nothing smart happening here.
• Agda.Interaction.Options.Warnings
• Agda.Interaction.Output
• Agda.Interaction.Response
• Agda.Interaction.Response.BaseData type for all interactive responses
• Agda.Interaction.SearchAbout
• Agda.MainAgda main module.
• Agda.Mimer.MimerThis module contains the implementation of Mimer, the current
• Agda.Mimer.Options
• Agda.SetupAgda's self-setup.
• Agda.Setup.DataFilesThe list of data files Agda uses. Because of TemplateHaskell state restrictions, this cannot be define in 'Agda.Setup'.
• Agda.Setup.EmacsModeSetup up the emacs mode for Agda.
• Agda.Syntax.AbstractThe abstract syntax. This is what you get after desugaring and scope
• Agda.Syntax.Abstract.NameAbstract names carry unique identifiers and stuff.
• Agda.Syntax.Abstract.PatternAuxiliary functions to handle patterns in the abstract syntax. Generic and specific traversals.
• Agda.Syntax.Abstract.PatternSynonymsPattern synonym utilities: folding pattern synonym definitions for
• Agda.Syntax.Abstract.Pretty
• Agda.Syntax.Abstract.UsedNames
• Agda.Syntax.Abstract.Views
• Agda.Syntax.BuiltinThis module defines the names of all builtin and primitives used in Agda. See Agda.TypeChecking.Monad.Builtin
• Agda.Syntax.CommonSome common syntactic entities are defined in this module.
• Agda.Syntax.Common.Aspect
• Agda.Syntax.Common.KeywordRangeA abstract Range type dedicated to keyword occurrences in the source.
• Agda.Syntax.Common.PrettyPretty printing functions.
• Agda.Syntax.Common.Pretty.ANSI
• Agda.Syntax.ConcreteThe concrete syntax is a raw representation of the program text
• Agda.Syntax.Concrete.Attribute
• Agda.Syntax.Concrete.DefinitionsPreprocess Declarations, producing NiceDeclarations. Attach fixity and syntax declarations to the definition they refer to. Distribute t…
• Agda.Syntax.Concrete.Definitions.Errors
• Agda.Syntax.Concrete.Definitions.Monad
• Agda.Syntax.Concrete.Definitions.Types
• Agda.Syntax.Concrete.FixityCollecting fixity declarations (and polarity pragmas) for concrete
• Agda.Syntax.Concrete.GenericGeneric traversal and reduce for concrete syntax,
• Agda.Syntax.Concrete.GlyphChoice of Unicode or ASCII glyphs.
• Agda.Syntax.Concrete.NameNames in the concrete syntax are just strings (or lists of strings for
• Agda.Syntax.Concrete.OperatorsThe parser doesn't know about operators and parses everything as normal
• Agda.Syntax.Concrete.Operators.Parser
• Agda.Syntax.Concrete.Operators.Parser.MonadThe parser monad used by the operator parser
• Agda.Syntax.Concrete.PatternTools for patterns in concrete syntax.
• Agda.Syntax.Concrete.PrettyPretty printer for the concrete syntax.
• Agda.Syntax.DoNotationDesugaring for do-notation. Uses whatever `_>>=_` and `_>>_` happen to be
• Agda.Syntax.FixityDefinitions for fixity, precedence levels, and declared syntax.
• Agda.Syntax.IdiomBrackets
• Agda.Syntax.InfoAn info object contains additional information about a piece of abstract
• Agda.Syntax.Literal
• Agda.Syntax.NotationAs a concrete name, a notation is a non-empty list of alternating IdParts and holes.
• Agda.Syntax.Parser
• Agda.Syntax.Parser.AlexThis module defines the things required by Alex and some other
• Agda.Syntax.Parser.CommentsThis module defines the lex action to lex nested comments. As is well-known
• Agda.Syntax.Parser.HelpersUtility functions used in the Happy parser.
• Agda.Syntax.Parser.LayoutThis module contains the lex actions that handle the layout rules. The way
• Agda.Syntax.Parser.LexActionsThis module contains the building blocks used to construct the lexer.
• Agda.Syntax.Parser.LexerThe lexer is generated by Alex (http://www.haskell.org/alex) and is an
• Agda.Syntax.Parser.LiteratePreprocessors for literate code formats.
• Agda.Syntax.Parser.LookAheadWhen lexing by hand (for instance string literals) we need to do some
• Agda.Syntax.Parser.Monad
• Agda.Syntax.Parser.ParserThe parser is generated by Happy (http://www.haskell.org/happy).
• Agda.Syntax.Parser.StringLiteralsThe code to lex string and character literals. Basically the same code
• Agda.Syntax.Parser.Tokens
• Agda.Syntax.PositionPosition information for syntax. Crucial for giving good error messages.
• Agda.Syntax.Reflected
• Agda.Syntax.Scope.BaseThis module defines the notion of a scope and operations on scopes.
• Agda.Syntax.Scope.FlatFlattened scopes.
• Agda.Syntax.Scope.MonadThe scope monad with operations.
• Agda.Syntax.TopLevelModuleName
• Agda.Syntax.TopLevelModuleName.Boot
• Agda.Syntax.Translation.AbstractToConcreteThe translation of abstract syntax to concrete syntax has two purposes.
• Agda.Syntax.Translation.ConcreteToAbstractTranslation from Agda.Syntax.Concrete to Agda.Syntax.Abstract.
• Agda.Syntax.Translation.InternalToAbstractTranslating from internal syntax to abstract syntax. Enables nice
• Agda.Syntax.Translation.ReflectedToAbstract
• Agda.Syntax.TreelessThe treeless syntax is intended to be used as input for the compiler backends.
• Agda.Termination.CallGraphCall graphs and related concepts, more or less as defined in
• Agda.Termination.CallMatrix
• Agda.Termination.CutOffDefines CutOff type which is used in Agda.Interaction.Options.
• Agda.Termination.MonadThe monad for the termination checker. The termination monad TerM is an extension of
• Agda.Termination.OrderAn Abstract domain of relative sizes, i.e., differences
• Agda.Termination.RecCheckChecking for recursion: We detect truly (co)recursive definitions by computing the
• Agda.Termination.SemiringSemirings.
• Agda.Termination.SparseMatrixSparse matrices. We assume the matrices to be very sparse, so we just implement them as
• Agda.Termination.TermCheck
• Agda.Termination.TerminationTermination checker, based on
• Agda.TheTypeChecker
• Agda.TypeChecking.AbstractFunctions for abstracting terms over other terms.
• Agda.TypeChecking.CheckInternalA bidirectional type checker for internal syntax. Performs checking on unreduced terms.
• Agda.TypeChecking.CompiledClauseCase trees. After coverage checking, pattern matching is translated
• Agda.TypeChecking.CompiledClause.Compile
• Agda.TypeChecking.CompiledClause.Match
• Agda.TypeChecking.Constraints
• Agda.TypeChecking.Conversion
• Agda.TypeChecking.Conversion.Pure
• Agda.TypeChecking.CoverageCoverage checking, case splitting, and splitting for refine tactics.
• Agda.TypeChecking.Coverage.Cubical
• Agda.TypeChecking.Coverage.MatchGiven 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.SplitClauseSplitClause and CoverResult types.
• Agda.TypeChecking.Coverage.SplitTreeSplit tree for transforming pattern clauses into case trees. The coverage checker generates a split tree from the clauses.
• Agda.TypeChecking.Datatypes
• Agda.TypeChecking.DeadCode
• Agda.TypeChecking.DiscrimTreeImperfect discrimination trees for indexing data by internal
• Agda.TypeChecking.DiscrimTree.Types
• Agda.TypeChecking.DisplayFormTools for DisplayTerm and DisplayForm.
• Agda.TypeChecking.DropArgs
• Agda.TypeChecking.Empty
• Agda.TypeChecking.Errors
• Agda.TypeChecking.Errors.NamesConvert errors to their names.
• Agda.TypeChecking.EtaContractCompute eta short normal forms.
• Agda.TypeChecking.ForcingA constructor argument is forced if it appears as pattern variable
• Agda.TypeChecking.FreeComputing the free variables of a term. The distinction between rigid and strongly rigid occurrences comes from:
• Agda.TypeChecking.Free.LazyComputing the free variables of a term lazily. We implement a reduce (traversal into monoid) over internal syntax
• Agda.TypeChecking.Free.PrecomputePrecompute free variables in a term (and store in ArgInfo).
• Agda.TypeChecking.Free.ReduceFree variable check that reduces the subject to make certain variables not
• Agda.TypeChecking.Functions
• Agda.TypeChecking.GeneralizeThis module implements the type checking part of generalisable variables. When we get here we have
• Agda.TypeChecking.IApplyConfluence
• Agda.TypeChecking.ImplicitFunctions for inserting implicit arguments at the right places.
• Agda.TypeChecking.InjectivityInjectivity, or more precisely, "constructor headedness", is a
• Agda.TypeChecking.InliningLogic for deciding which functions should be automatically inlined.
• Agda.TypeChecking.InstanceArguments
• Agda.TypeChecking.IrrelevanceCompile-time irrelevance. In type theory with compile-time irrelevance à la Pfenning (LiCS 2001),
• Agda.TypeChecking.Level
• Agda.TypeChecking.Level.Solve
• Agda.TypeChecking.LevelConstraints
• Agda.TypeChecking.Lock
• Agda.TypeChecking.MetaVars
• Agda.TypeChecking.MetaVars.Mention
• Agda.TypeChecking.MetaVars.OccursThe occurs check for unification. Does pruning on the fly. When hitting a meta variable: Compute flex/rigid for its arguments. Compare …
• Agda.TypeChecking.Modalities
• Agda.TypeChecking.Monad
• Agda.TypeChecking.Monad.Base
• Agda.TypeChecking.Monad.Base.TypesData structures for the type checker. Part of Agda.TypeChecking.Monad.Base, extracted to avoid import cycles.
• Agda.TypeChecking.Monad.Base.WarningTypes related to warnings raised by Agda.
• Agda.TypeChecking.Monad.BenchmarkMeasure CPU time for individual phases of the Agda pipeline.
• Agda.TypeChecking.Monad.Builtin
• Agda.TypeChecking.Monad.Caching
• Agda.TypeChecking.Monad.Closure
• Agda.TypeChecking.Monad.Constraints
• Agda.TypeChecking.Monad.Context
• Agda.TypeChecking.Monad.Debug
• Agda.TypeChecking.Monad.Env
• Agda.TypeChecking.Monad.Imports
• Agda.TypeChecking.Monad.MetaVars
• Agda.TypeChecking.Monad.ModalityModality. Agda has support for several modalities, namely: Cohesion Quantity Relevance In order to type check such modalities, we must …
• Agda.TypeChecking.Monad.Mutual
• Agda.TypeChecking.Monad.Open
• Agda.TypeChecking.Monad.Options
• Agda.TypeChecking.Monad.PureA typeclass collecting all pure typechecking operations
• Agda.TypeChecking.Monad.Signature
• Agda.TypeChecking.Monad.SizedTypesStuff for sized types that does not require modules
• Agda.TypeChecking.Monad.StateLenses for TCState and more.
• Agda.TypeChecking.Monad.StatisticsCollect statistics.
• Agda.TypeChecking.Monad.Trace
• Agda.TypeChecking.NamesEDSL 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.Opacity
• Agda.TypeChecking.Patterns.AbstractTools to manipulate patterns in abstract syntax
• Agda.TypeChecking.Patterns.MatchPattern matcher used in the reducer for clauses that
• Agda.TypeChecking.PolarityComputing the polarity (variance) of function arguments,
• Agda.TypeChecking.PositivityCheck that a datatype is strictly positive.
• Agda.TypeChecking.Positivity.OccurrenceOccurrences.
• Agda.TypeChecking.Pretty
• Agda.TypeChecking.Pretty.Call
• Agda.TypeChecking.Pretty.Constraint
• Agda.TypeChecking.Pretty.Warning
• Agda.TypeChecking.PrimitivePrimitive functions, such as addition on builtin integers.
• Agda.TypeChecking.Primitive.Base
• Agda.TypeChecking.Primitive.Cubical
• Agda.TypeChecking.Primitive.Cubical.BaseImplementations of the basic primitives of Cubical Agda: The
• Agda.TypeChecking.Primitive.Cubical.Glue
• Agda.TypeChecking.Primitive.Cubical.HCompU
• Agda.TypeChecking.ProjectionLikeDropping initial arguments (`parameters') from a function which can be
• Agda.TypeChecking.Quote
• Agda.TypeChecking.ReconstructParametersReconstruct dropped parameters from constructors. Used by
• Agda.TypeChecking.RecordPatternsCode which replaces pattern matching on record constructors with
• Agda.TypeChecking.Records
• Agda.TypeChecking.Reduce
• Agda.TypeChecking.Reduce.FastThis module implements the Agda Abstract Machine used for compile-time reduction. It's a
• Agda.TypeChecking.Reduce.Monad
• Agda.TypeChecking.RewritingRewriting with arbitrary rules. The user specifies a relation symbol by the pragma
• Agda.TypeChecking.Rewriting.Clause
• Agda.TypeChecking.Rewriting.ConfluenceChecking local or global confluence of rewrite rules. For checking LOCAL CONFLUENCE of a given rewrite rule f ps ↦ v,
• Agda.TypeChecking.Rewriting.NonLinMatchNon-linear matching of the lhs of a rewrite rule against a
• Agda.TypeChecking.Rewriting.NonLinPatternVarious utility functions dealing with the non-linear, higher-order
• Agda.TypeChecking.Rules.Application
• Agda.TypeChecking.Rules.Builtin
• Agda.TypeChecking.Rules.Builtin.CoinductionHandling of the INFINITY, SHARP and FLAT builtins.
• Agda.TypeChecking.Rules.Data
• Agda.TypeChecking.Rules.Decl
• Agda.TypeChecking.Rules.Def
• Agda.TypeChecking.Rules.Display
• Agda.TypeChecking.Rules.LHS
• Agda.TypeChecking.Rules.LHS.Implicit
• Agda.TypeChecking.Rules.LHS.Problem
• Agda.TypeChecking.Rules.LHS.ProblemRest
• Agda.TypeChecking.Rules.LHS.UnifyUnification algorithm for specializing datatype indices, as described in
• Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
• Agda.TypeChecking.Rules.LHS.Unify.Types
• Agda.TypeChecking.Rules.Record
• Agda.TypeChecking.Rules.Term
• Agda.TypeChecking.SerialiseStructure-sharing serialisation of Agda interface files.
• Agda.TypeChecking.Serialise.Base
• Agda.TypeChecking.Serialise.Instances
• Agda.TypeChecking.Serialise.Instances.Abstract
• Agda.TypeChecking.Serialise.Instances.Common
• Agda.TypeChecking.Serialise.Instances.Compilers
• Agda.TypeChecking.Serialise.Instances.Errors
• Agda.TypeChecking.Serialise.Instances.Highlighting
• Agda.TypeChecking.SizedTypes
• Agda.TypeChecking.SizedTypes.Pretty
• Agda.TypeChecking.SizedTypes.SolveSolving size constraints under hypotheses. The size solver proceeds as follows: Get size constraints, cluster into connected components. …
• Agda.TypeChecking.SizedTypes.SyntaxSyntax of size expressions and constraints.
• Agda.TypeChecking.SizedTypes.Utils
• Agda.TypeChecking.SizedTypes.WarshallSolver
• Agda.TypeChecking.SortThis module contains the rules for Agda's sort system viewed as a pure
• Agda.TypeChecking.SubstituteThis module contains the definition of hereditary substitution
• Agda.TypeChecking.Substitute.Class
• Agda.TypeChecking.Substitute.DeBruijn
• Agda.TypeChecking.SyntacticEqualityA syntactic equality check that takes meta instantiations into account,
• Agda.TypeChecking.Telescope
• Agda.TypeChecking.Telescope.Path
• Agda.TypeChecking.Unquote
• Agda.TypeChecking.Warnings
• Agda.TypeChecking.With
• Agda.Utils.AffineHoleContexts with at most one hole.
• Agda.Utils.Applicative
• Agda.Utils.AssocListAdditional functions for association lists.
• Agda.Utils.BagA simple overlay over Data.Map to manage unordered sets with duplicates.
• Agda.Utils.BenchmarkTools for benchmarking and accumulating results.
• Agda.Utils.BiMapPartly invertible finite maps. Time complexities are given under the assumption that all relevant
• Agda.Utils.BoolSetRepresentation 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.BooleanBoolean algebras and types isomorphic to Bool. There are already solutions for Boolean algebras in the Haskell ecosystem,
• Agda.Utils.CallStack
• Agda.Utils.CharAgda strings uses Data.Text [1], which can only represent unicode scalar values [2], excluding
• Agda.Utils.ClusterCreate clusters of non-overlapping things.
• Agda.Utils.EitherUtilities for the Either type.
• Agda.Utils.EmptyAn empty type with some useful instances.
• Agda.Utils.EnvironmentExpand environment variables in strings
• Agda.Utils.FailA pure MonadFail.
• Agda.Utils.FavoritesMaintaining a list of favorites of some partially ordered type.
• Agda.Utils.FileIdTranslating between file paths and ids. This module allows you to build a dictionary from file paths to some unique identifier
• Agda.Utils.FileNameOperations on file names.
• Agda.Utils.FloatLogically consistent comparison of floating point numbers.
• Agda.Utils.Function
• Agda.Utils.FunctorUtilities for functors.
• Agda.Utils.GetOptThis module provides facilities for parsing the command-line options
• Agda.Utils.Graph.AdjacencyMap.UnidirectionalDirected graphs (can of course simulate undirected graphs). Represented as adjacency maps in direction from source to target. Each source…
• Agda.Utils.Graph.TopSort
• Agda.Utils.HashInstead of checking time-stamps we compute a hash of the module source and
• Agda.Utils.HashTableHash tables.
• Agda.Utils.Haskell.SyntaxASTs for subset of GHC Haskell syntax.
• Agda.Utils.IArrayArray utilities.
• Agda.Utils.IOAuxiliary functions for the IO monad.
• Agda.Utils.IO.BinaryBinary IO.
• Agda.Utils.IO.Directory
• Agda.Utils.IO.TempFileCommon syntax highlighting functions for Emacs and JSON
• Agda.Utils.IO.UTF8Text IO using the UTF8 character encoding.
• Agda.Utils.IORefUtilities for Data.IORef.
• Agda.Utils.ImpossibleAn interface for reporting "impossible" errors
• Agda.Utils.IndexedList
• Agda.Utils.IntSet.InfinitePossibly infinite sets of integers (but with finitely many consecutive
• Agda.Utils.LensA cut-down implementation of lenses, with names taken from
• Agda.Utils.Lens.ExamplesExamples how to use Agda.Utils.Lens.
• Agda.Utils.ListUtility functions for lists.
• Agda.Utils.List1Non-empty lists. Better name List1 for non-empty lists, plus missing functionality. Import:
• Agda.Utils.List2Lists of length at least 2. Import as:
• Agda.Utils.ListTListT done right,
• Agda.Utils.Map
• Agda.Utils.Map1Non-empty maps. Provides type Map1 of non-empty maps. Import:
• Agda.Utils.MaybeExtend Maybe by common operations for the Maybe type. Note: since this module is usually imported unqualified,
• Agda.Utils.Maybe.StrictA strict version of the Maybe type. Import qualified, as in
• Agda.Utils.Memo
• Agda.Utils.Monad
• Agda.Utils.MonoidMore monoids.
• Agda.Utils.NullOverloaded null and empty for collections and sequences.
• Agda.Utils.POMonoidPartially ordered monoids.
• Agda.Utils.Parser.MemoisedCPSParser combinators with support for left recursion, following
• Agda.Utils.PartialOrd
• Agda.Utils.Permutation
• Agda.Utils.ProfileOptions
• Agda.Utils.RangeMapMaps containing non-overlapping intervals.
• Agda.Utils.SemiRing
• Agda.Utils.SemigroupSome semigroup instances used in several places
• Agda.Utils.Set1Non-empty sets. Provides type Set1 of non-empty sets. Import:
• Agda.Utils.SingletonConstructing singleton collections.
• Agda.Utils.SizeCollection size. For TermSize see Agda.Syntax.Internal.
• Agda.Utils.SmallSetSmall sets represented as a bitmask for fast membership checking. With the exception of converting to/from lists, all operations are O(1)…
• Agda.Utils.String
• Agda.Utils.Suffix
• Agda.Utils.ThreeTools for 3-way partitioning.
• Agda.Utils.TimeTime-related utilities.
• Agda.Utils.TrieStrict tries (based on Data.Map.Strict and Agda.Utils.Maybe.Strict). Note that if delete or adjust are used, one may end up with non-cano…
• Agda.Utils.Tuple
• Agda.Utils.TypeLevel
• Agda.Utils.TypeLitsType level literals, inspired by GHC.TypeLits.
• Agda.Utils.Unsafe
• Agda.Utils.Update
• Agda.Utils.VarSetManage sets of natural numbers (de Bruijn indices).
• Agda.Utils.WithDefaultPotentially uninitialised Booleans. The motivation for this small library is to distinguish
• Agda.Utils.Zipper
• Agda.Version
• Agda.VersionCommit

• STMonadTrans-0.4.8.1in this set
• aeson-2.2.5.1in this set
• ansi-terminal-1.1.5in this set
• array-0.5.8.0with GHC
• async-2.2.6in this set
• base-4.23.0.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.8with GHC
• data-hash-0.2.0.1in this set
• deepseq-1.5.2.0with GHC
• directory-1.3.11.0with GHC
• dlist-1.0in this set
• edit-distance-0.2.2.1in this set
• enummapset-0.7.3.0in this set
• equivalence-0.4.1.1in this set
• exceptions-0.10.12with GHC
• filelock-0.1.1.9in this set
• filemanip-0.3.6.3in this set
• filepath-1.5.5.0with GHC
• generic-data-1.1.0.2in this set
• ghc-compact-0.1.0.0with GHC
• hashable-1.5.1.0in this set
• haskeline-0.8.5.0with GHC
• monad-control-1.0.3.1in this set
• mtl-2.3.2with GHC
• murmur-hash-0.1.0.11in this set
• nonempty-containers-0.3.6.0in this set
• parallel-3.3.0.0in this set
• peano-0.1.1.0in this set
• pqueue-1.7.0.0in this set
• pretty-1.1.3.6with GHC
• process-1.6.30.0with GHC
• process-extras-0.7.4in this set
• regex-tdfa-1.3.2.6in this set
• split-0.2.5.1in this set
• stm-2.5.3.1with GHC
• strict-0.5.1in this set
• template-haskell-2.25.0.0with GHC
• text-2.1.4with GHC
• time-1.16.0.1with GHC
• transformers-0.6.3.0with 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.1in this set
• zlib-0.7.1.1in this set

Used by in this set · 0

Nothing in this set depends on it.