# Agda

A dependently typed functional programming language and proof assistant

http://wiki.portal.chalmers.se/agda/

Version on this page: | 2.6.2 |

LTS Haskell 22.34: | 2.6.4.3@rev:1 |

Stackage Nightly 2024-09-17: | 2.7.0.1 |

Latest on Hackage: | 2.7.0.1 |

Maintained by

**Ulf Norell**This version can be pinned in stack with:

`Agda-2.6.2@sha256:4119e4477b39807934295a46ca2ade58f861963501683e6687869602d4315fd8,36202`

#### Module documentation for 2.6.2

- Agda
- Agda.Auto
- Agda.Benchmarking
- Agda.Compiler
- Agda.Compiler.Backend
- Agda.Compiler.Builtin
- Agda.Compiler.CallCompiler
- Agda.Compiler.Common
- Agda.Compiler.JS
- Agda.Compiler.MAlonzo
- Agda.Compiler.ToTreeless
- Agda.Compiler.Treeless
- Agda.Compiler.Treeless.AsPatterns
- Agda.Compiler.Treeless.Builtin
- Agda.Compiler.Treeless.Compare
- Agda.Compiler.Treeless.EliminateDefaults
- Agda.Compiler.Treeless.EliminateLiteralPatterns
- Agda.Compiler.Treeless.Erase
- Agda.Compiler.Treeless.GuardsToPrims
- Agda.Compiler.Treeless.Identity
- Agda.Compiler.Treeless.NormalizeNames
- Agda.Compiler.Treeless.Pretty
- Agda.Compiler.Treeless.Simplify
- Agda.Compiler.Treeless.Subst
- Agda.Compiler.Treeless.Uncase
- Agda.Compiler.Treeless.Unused

- Agda.ImpossibleTest
- Agda.Interaction
- Agda.Interaction.AgdaTop
- Agda.Interaction.Base
- Agda.Interaction.BasicOps
- Agda.Interaction.CommandLine
- Agda.Interaction.EmacsCommand
- Agda.Interaction.EmacsTop
- Agda.Interaction.ExitCode
- Agda.Interaction.FindFile
- Agda.Interaction.Highlighting
- Agda.Interaction.Highlighting.Common
- Agda.Interaction.Highlighting.Dot
- Agda.Interaction.Highlighting.Emacs
- Agda.Interaction.Highlighting.FromAbstract
- Agda.Interaction.Highlighting.Generate
- Agda.Interaction.Highlighting.HTML
- Agda.Interaction.Highlighting.JSON
- Agda.Interaction.Highlighting.LaTeX
- Agda.Interaction.Highlighting.Precise
- Agda.Interaction.Highlighting.Range
- Agda.Interaction.Highlighting.Vim

- Agda.Interaction.Imports
- Agda.Interaction.InteractionTop
- Agda.Interaction.JSON
- Agda.Interaction.JSONTop
- Agda.Interaction.Library
- Agda.Interaction.MakeCase
- Agda.Interaction.Monad
- Agda.Interaction.Options
- Agda.Interaction.Response
- Agda.Interaction.SearchAbout

- Agda.Main
- Agda.Syntax
- Agda.Syntax.Abstract
- Agda.Syntax.Builtin
- Agda.Syntax.Common
- Agda.Syntax.Concrete
- Agda.Syntax.DoNotation
- Agda.Syntax.Fixity
- Agda.Syntax.IdiomBrackets
- Agda.Syntax.Info
- Agda.Syntax.Internal
- Agda.Syntax.Literal
- Agda.Syntax.Notation
- Agda.Syntax.Parser
- Agda.Syntax.Parser.Alex
- Agda.Syntax.Parser.Comments
- Agda.Syntax.Parser.Layout
- Agda.Syntax.Parser.LexActions
- Agda.Syntax.Parser.Lexer
- Agda.Syntax.Parser.Literate
- Agda.Syntax.Parser.LookAhead
- Agda.Syntax.Parser.Monad
- Agda.Syntax.Parser.Parser
- Agda.Syntax.Parser.StringLiterals
- Agda.Syntax.Parser.Tokens

- Agda.Syntax.Position
- Agda.Syntax.Reflected
- Agda.Syntax.Scope
- Agda.Syntax.Translation
- Agda.Syntax.Treeless

- Agda.Termination
- Agda.TheTypeChecker
- Agda.TypeChecking
- Agda.TypeChecking.Abstract
- Agda.TypeChecking.CheckInternal
- Agda.TypeChecking.CompiledClause
- Agda.TypeChecking.Constraints
- Agda.TypeChecking.Conversion
- Agda.TypeChecking.Coverage
- Agda.TypeChecking.Datatypes
- Agda.TypeChecking.DeadCode
- Agda.TypeChecking.DisplayForm
- Agda.TypeChecking.DropArgs
- Agda.TypeChecking.Empty
- Agda.TypeChecking.Errors
- Agda.TypeChecking.EtaContract
- Agda.TypeChecking.EtaExpand
- Agda.TypeChecking.Forcing
- Agda.TypeChecking.Free
- Agda.TypeChecking.Functions
- Agda.TypeChecking.Generalize
- Agda.TypeChecking.IApplyConfluence
- Agda.TypeChecking.Implicit
- Agda.TypeChecking.Injectivity
- Agda.TypeChecking.Inlining
- Agda.TypeChecking.InstanceArguments
- Agda.TypeChecking.Irrelevance
- Agda.TypeChecking.Level
- Agda.TypeChecking.LevelConstraints
- Agda.TypeChecking.Lock
- Agda.TypeChecking.MetaVars
- Agda.TypeChecking.Monad
- Agda.TypeChecking.Monad.Base
- Agda.TypeChecking.Monad.Benchmark
- 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.Mutual
- Agda.TypeChecking.Monad.Open
- Agda.TypeChecking.Monad.Options
- Agda.TypeChecking.Monad.Pure
- Agda.TypeChecking.Monad.Signature
- Agda.TypeChecking.Monad.SizedTypes
- Agda.TypeChecking.Monad.State
- Agda.TypeChecking.Monad.Statistics
- Agda.TypeChecking.Monad.Trace

- Agda.TypeChecking.Names
- Agda.TypeChecking.Patterns
- Agda.TypeChecking.Polarity
- Agda.TypeChecking.Positivity
- Agda.TypeChecking.Pretty
- Agda.TypeChecking.Primitive
- Agda.TypeChecking.ProjectionLike
- Agda.TypeChecking.Quote
- Agda.TypeChecking.ReconstructParameters
- Agda.TypeChecking.RecordPatterns
- Agda.TypeChecking.Records
- Agda.TypeChecking.Reduce
- Agda.TypeChecking.Rewriting
- Agda.TypeChecking.Rules
- Agda.TypeChecking.Serialise
- Agda.TypeChecking.SizedTypes
- Agda.TypeChecking.Sort
- Agda.TypeChecking.Substitute
- Agda.TypeChecking.SyntacticEquality
- Agda.TypeChecking.Telescope
- Agda.TypeChecking.Unquote
- Agda.TypeChecking.Warnings
- Agda.TypeChecking.With

- Agda.Utils
- Agda.Utils.AffineHole
- Agda.Utils.Applicative
- Agda.Utils.AssocList
- Agda.Utils.Bag
- Agda.Utils.Benchmark
- Agda.Utils.BiMap
- Agda.Utils.CallStack
- Agda.Utils.Char
- Agda.Utils.Cluster
- Agda.Utils.Either
- Agda.Utils.Empty
- Agda.Utils.Environment
- Agda.Utils.Fail
- Agda.Utils.Favorites
- Agda.Utils.FileName
- Agda.Utils.Float
- Agda.Utils.Function
- Agda.Utils.Functor
- Agda.Utils.Graph
- Agda.Utils.Graph.AdjacencyMap
- Agda.Utils.Graph.TopSort

- Agda.Utils.Hash
- Agda.Utils.Haskell
- Agda.Utils.IO
- Agda.Utils.IORef
- Agda.Utils.Impossible
- Agda.Utils.IndexedList
- Agda.Utils.IntSet
- Agda.Utils.Lens
- Agda.Utils.List
- Agda.Utils.List1
- Agda.Utils.List2
- Agda.Utils.ListT
- Agda.Utils.Map
- Agda.Utils.Maybe
- Agda.Utils.Memo
- Agda.Utils.Monad
- Agda.Utils.Monoid
- Agda.Utils.Null
- Agda.Utils.POMonoid
- Agda.Utils.Parser
- Agda.Utils.PartialOrd
- Agda.Utils.Permutation
- Agda.Utils.Pointer
- Agda.Utils.Pretty
- Agda.Utils.RangeMap
- Agda.Utils.SemiRing
- Agda.Utils.Semigroup
- Agda.Utils.Singleton
- Agda.Utils.Size
- Agda.Utils.SmallSet
- Agda.Utils.String
- Agda.Utils.Suffix
- Agda.Utils.Three
- Agda.Utils.Time
- Agda.Utils.Trie
- Agda.Utils.Tuple
- Agda.Utils.TypeLevel
- Agda.Utils.TypeLits
- Agda.Utils.Update
- Agda.Utils.VarSet
- Agda.Utils.Warshall
- Agda.Utils.WithDefault
- Agda.Utils.Zipper

- Agda.Version
- Agda.VersionCommit

Depends on 40 packages

*(full list with versions)*:aeson, Agda, array, async, base, binary, blaze-html, boxes, bytestring, case-insensitive, containers, data-hash, deepseq, directory, edit-distance, equivalence, exceptions, filepath, ghc-compact, gitrev, hashable, hashtables, haskeline, monad-control, mtl, murmur-hash, parallel, pretty, process, regex-tdfa, split, stm, strict, template-haskell, text, time, transformers, unordered-containers, uri-encode, zlib