Package2.8.0.2Dependent types

Agda

A dependently typed functional programming language and proof assistant

Version2.8.0.2
CategoryDependent types
LicenceMIT
AuthorThe Agda Team, see https://agda.readthedocs.io/en/latest/team.html
MaintainerThe Agda Team
Homepagewiki.portal.chalmers.se/agda
Pinned byhackage Agda 2.8.0.2
Sourcehackage.haskell.org/package/Agda-2.8.0.2

Modules

384 modules

Agda.Benchmarking9Agda-specific benchmarking structure.
Agda.Compiler.Backend14Interface for compiler backend writers.
Agda.Compiler.Backend.Base7
Agda.Compiler.Builtin1Built-in backends.
Agda.Compiler.CallCompiler2A command which calls a compiler
Agda.Compiler.Common12
Agda.Compiler.JS.Compiler40Main module for JS backend.
Agda.Compiler.JS.Pretty31
Agda.Compiler.JS.Substitution19
Agda.Compiler.JS.Syntax10
Agda.Compiler.MAlonzo.Coerce2
Agda.Compiler.MAlonzo.Compiler2
Agda.Compiler.MAlonzo.Encode1
Agda.Compiler.MAlonzo.HaskellTypes3Translating Agda types to Haskell types. Used to ensure that imported
Agda.Compiler.MAlonzo.Misc67
Agda.Compiler.MAlonzo.Pragmas13
Agda.Compiler.MAlonzo.Pretty6
Agda.Compiler.MAlonzo.Primitives11
Agda.Compiler.MAlonzo.Strict1Strictification of Haskell code
Agda.Compiler.ToTreeless9
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.Base28
Agda.Interaction.BasicOps49
Agda.Interaction.BuildLibrary1Type-check all files of a library (option --build-library).
Agda.Interaction.Command5
Agda.Interaction.CommandLine1
Agda.Interaction.EmacsCommand7Code for instructing Emacs to do things
Agda.Interaction.EmacsTop7
Agda.Interaction.ExitCode5
Agda.Interaction.FindFile19Functions 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.Dot.Backend1
Agda.Interaction.Highlighting.Dot.Base3Generate an import dependency graph for a given module.
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.HTML.Backend1Backend for generating highlighted, hyperlinked HTML from Agda sources.
Agda.Interaction.Highlighting.HTML.Base8Function for generating highlighted, hyperlinked HTML from Agda
Agda.Interaction.Highlighting.JSON1Functions which give precise syntax highlighting info in JSON format.
Agda.Interaction.Highlighting.LaTeX0Generating highlighted and aligned LaTeX from literate Agda source.
Agda.Interaction.Highlighting.LaTeX.Backend1
Agda.Interaction.Highlighting.LaTeX.Base6Function for generating highlighted and aligned LaTeX from literate
Agda.Interaction.Highlighting.Precise22Types used for precise syntax highlighting.
Agda.Interaction.Highlighting.Range12Ranges.
Agda.Interaction.Highlighting.Vim8
Agda.Interaction.Imports20This module deals with finding imported modules and loading their
Agda.Interaction.InteractionTop41
Agda.Interaction.JSON115Encoding stuff into JSON values in TCM
Agda.Interaction.JSONTop1
Agda.Interaction.Library24Library management. Sample use: -- Get libraries as listed in .agda/libraries file.
Agda.Interaction.Library.Base46Basic 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.Options194
Agda.Interaction.Options.Errors39Provide names for the errors Agda throws.Options/Er
Agda.Interaction.Options.Help4
Agda.Interaction.Options.Lenses19Lenses 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.Main21Agda main module.
Agda.Mimer.Mimer2This module contains the implementation of Mimer, the current
Agda.Mimer.Options9
Agda.Setup4Agda's self-setup.
Agda.Setup.DataFiles4The list of data files Agda uses. Because of TemplateHaskell state restrictions, this cannot be define in 'Agda.Setup'.
Agda.Setup.EmacsMode8Setup up the emacs mode for Agda.
Agda.Syntax.Abstract85The abstract syntax. This is what you get after desugaring and scope
Agda.Syntax.Abstract.Name47Abstract names carry unique identifiers and stuff.
Agda.Syntax.Abstract.Pattern31Auxiliary 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.Pretty6
Agda.Syntax.Abstract.UsedNames1
Agda.Syntax.Abstract.Views25
Agda.Syntax.Builtin226This module defines the names of all builtin and primitives used in Agda. See Agda.TypeChecking.Monad.Builtin
Agda.Syntax.Common312Some 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.Pretty85Pretty printing functions.
Agda.Syntax.Common.Pretty.ANSI2
Agda.Syntax.Concrete88The concrete syntax is a raw representation of the program text
Agda.Syntax.Concrete.Attribute27
Agda.Syntax.Concrete.Definitions16Preprocess Declarations, producing NiceDeclarations. Attach fixity and syntax declarations to the definition they refer to. Distribute t…
Agda.Syntax.Concrete.Definitions.Errors11
Agda.Syntax.Concrete.Definitions.Monad36
Agda.Syntax.Concrete.Definitions.Types26
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.Pretty13Pretty 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.Helpers63Utility 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.Literate14Preprocessors 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.Position60Position information for syntax. Crucial for giving good error messages.
Agda.Syntax.Reflected12
Agda.Syntax.Scope.Base136This module defines the notion of a scope and operations on scopes.
Agda.Syntax.Scope.Flat4Flattened scopes.
Agda.Syntax.Scope.Monad76The scope monad with operations.
Agda.Syntax.TopLevelModuleName13
Agda.Syntax.TopLevelModuleName.Boot4
Agda.Syntax.Translation.AbstractToConcrete12The translation of abstract syntax to concrete syntax has two purposes.
Agda.Syntax.Translation.ConcreteToAbstract9Translation from Agda.Syntax.Concrete to Agda.Syntax.Abstract.
Agda.Syntax.Translation.InternalToAbstract7Translating from internal syntax to abstract syntax. Enables nice
Agda.Syntax.Translation.ReflectedToAbstract17
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.Termination6Termination 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.Pure9
Agda.TypeChecking.Coverage11Coverage checking, case splitting, and splitting for refine tactics.
Agda.TypeChecking.Coverage.Cubical6
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.Errors16
Agda.TypeChecking.Errors.Names13Convert errors to their names.
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.Implicit9Functions 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.InstanceArguments15
Agda.TypeChecking.Irrelevance11Compile-time irrelevance. In type theory with compile-time irrelevance à la Pfenning (LiCS 2001),
Agda.TypeChecking.Level24
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.Base671
Agda.TypeChecking.Monad.Base.Types23Data structures for the type checker. Part of Agda.TypeChecking.Monad.Base, extracted to avoid import cycles.
Agda.TypeChecking.Monad.Base.Warning2Types related to warnings raised by Agda.
Agda.TypeChecking.Monad.Benchmark9Measure CPU time for individual phases of the Agda pipeline.
Agda.TypeChecking.Monad.Builtin261
Agda.TypeChecking.Monad.Caching10
Agda.TypeChecking.Monad.Closure3
Agda.TypeChecking.Monad.Constraints34
Agda.TypeChecking.Monad.Context56
Agda.TypeChecking.Monad.Debug32
Agda.TypeChecking.Monad.Env26
Agda.TypeChecking.Monad.Imports15
Agda.TypeChecking.Monad.MetaVars79
Agda.TypeChecking.Monad.Modality17Modality. Agda has support for several modalities, namely: Cohesion Quantity Relevance In order to type check such modalities, we must …
Agda.TypeChecking.Monad.Mutual6
Agda.TypeChecking.Monad.Open4
Agda.TypeChecking.Monad.Options39
Agda.TypeChecking.Monad.Pure1A typeclass collecting all pure typechecking operations
Agda.TypeChecking.Monad.Signature100
Agda.TypeChecking.Monad.SizedTypes39Stuff for sized types that does not require modules
Agda.TypeChecking.Monad.State75Lenses for TCState and more.
Agda.TypeChecking.Monad.Statistics7Collect statistics.
Agda.TypeChecking.Monad.Trace8
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.Match18Pattern 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.Occurrence7Occurrences.
Agda.TypeChecking.Pretty47
Agda.TypeChecking.Pretty.Call1
Agda.TypeChecking.Pretty.Constraint4
Agda.TypeChecking.Pretty.Warning13
Agda.TypeChecking.Primitive40Primitive functions, such as addition on builtin integers.
Agda.TypeChecking.Primitive.Base44
Agda.TypeChecking.Primitive.Cubical40
Agda.TypeChecking.Primitive.Cubical.Base23Implementations of the basic primitives of Cubical Agda: The
Agda.TypeChecking.Primitive.Cubical.Glue5
Agda.TypeChecking.Primitive.Cubical.HCompU3
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.RecordPatterns4Code 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.Application8
Agda.TypeChecking.Rules.Builtin6
Agda.TypeChecking.Rules.Builtin.Coinduction6Handling of the INFINITY, SHARP and FLAT builtins.
Agda.TypeChecking.Rules.Data22
Agda.TypeChecking.Rules.Decl33
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.Term62
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.Class40
Agda.TypeChecking.Substitute.DeBruijn1
Agda.TypeChecking.SyntacticEquality4A syntactic equality check that takes meta instantiations into account,
Agda.TypeChecking.Telescope66
Agda.TypeChecking.Telescope.Path5
Agda.TypeChecking.Unquote35
Agda.TypeChecking.Warnings17
Agda.TypeChecking.With9
Agda.Utils.AffineHole1Contexts with at most one hole.
Agda.Utils.Applicative6
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.FileId12Translating between file paths and ids. This module allows you to build a dictionary from file paths to some unique identifier
Agda.Utils.FileName11Operations on file names.
Agda.Utils.Float43Logically consistent comparison of floating point numbers.
Agda.Utils.Function19
Agda.Utils.Functor8Utilities for functors.
Agda.Utils.GetOpt6This module provides facilities for parsing the command-line options
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.Directory3
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.Impossible7An interface for reporting "impossible" errors
Agda.Utils.IndexedList11
Agda.Utils.IntSet.Infinite10Possibly infinite sets of integers (but with finitely many consecutive
Agda.Utils.Lens26A cut-down implementation of lenses, with names taken from
Agda.Utils.Lens.Examples3Examples how to use Agda.Utils.Lens.
Agda.Utils.List76Utility functions for lists.
Agda.Utils.List1106Non-empty lists. Better name List1 for non-empty lists, plus missing functionality. Import:
Agda.Utils.List217Lists of length at least 2. Import as:
Agda.Utils.ListT18ListT done right,
Agda.Utils.Map2
Agda.Utils.Map1152Non-empty maps. Provides type Map1 of non-empty maps. Import:
Agda.Utils.Maybe29Extend Maybe by common operations for the Maybe type. Note: since this module is usually imported unqualified,
Agda.Utils.Maybe.Strict23A strict version of the Maybe type. Import qualified, as in
Agda.Utils.Memo4
Agda.Utils.Monad68
Agda.Utils.Monoid1More monoids.
Agda.Utils.Null11Overloaded 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.ProfileOptions8
Agda.Utils.RangeMap10Maps containing non-overlapping intervals.
Agda.Utils.SemiRing2
Agda.Utils.Semigroup1Some semigroup instances used in several places
Agda.Utils.Set180Non-empty sets. Provides type Set1 of non-empty sets. Import:
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.String11
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). Note that if delete or adjust are used, one may end up with non-cano…
Agda.Utils.Tuple15
Agda.Utils.TypeLevel25
Agda.Utils.TypeLits4Type level literals, inspired by GHC.TypeLits.
Agda.Utils.Unsafe1
Agda.Utils.Update15
Agda.Utils.VarSet21Manage sets of natural numbers (de Bruijn indices).
Agda.Utils.WithDefault7Potentially uninitialised Booleans. The motivation for this small library is to distinguish
Agda.Utils.Zipper3
Agda.Version3
Agda.VersionCommit2

Internal modules · 12

Agda.Syntax.Internal149
Agda.Syntax.Internal.Blockers34
Agda.Syntax.Internal.Defs5Extract used definitions from terms.
Agda.Syntax.Internal.Elim9
Agda.Syntax.Internal.Generic2Tree traversal for internal syntax.
Agda.Syntax.Internal.MetaVars7
Agda.Syntax.Internal.Names7Extract all names and meta-variables from things.
Agda.Syntax.Internal.Pattern20
Agda.Syntax.Internal.SanityCheck2Sanity checking for internal syntax. Mostly checking variable scoping.
Agda.Syntax.Internal.Univ8Kinds of standard universes: Prop, Type, SSet.
Agda.TypeChecking.Patterns.Internal2Tools to manipulate patterns in internal syntax
Agda.TypeChecking.Serialise.Instances.Internal2

Description

Agda is a dependently typed functional programming language: It has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code).

Agda is also a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Rocq (formerly known as Coq), Idris, Lean and NuPRL.

This package includes both a command-line program (agda) and an Emacs mode.

Depends on

50 packages

Used by in this set · 0

Nothing in this set depends on it.