Agda

A dependently typed functional programming language and proof assistant

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

Version on this page:	2.6.4.1
LTS Haskell 24.24:	2.8.0@rev:2
Stackage Nightly 2025-12-16:	2.8.0@rev:2
Latest on Hackage:	2.8.0@rev:2

See all snapshots Agda appears in

MIT licensed by The Agda Team, see https://agda.readthedocs.io/en/latest/team.html

Maintained by The Agda Team

This version can be pinned in stack with:Agda-2.6.4.1@sha256:be9841a3c57ea85b4931a14a692593f3283b7ae9712d0b612c161020fa221b48,29013

Module documentation for 2.6.4.1

Agda
- Agda.Auto
  - Agda.Auto.Auto
  - Agda.Auto.CaseSplit
  - Agda.Auto.Convert
  - Agda.Auto.NarrowingSearch
  - Agda.Auto.Options
  - Agda.Auto.SearchControl
  - Agda.Auto.Syntax
  - Agda.Auto.Typecheck
- Agda.Benchmarking
- Agda.Compiler
  - Agda.Compiler.Backend
  - Agda.Compiler.Builtin
  - Agda.Compiler.CallCompiler
  - Agda.Compiler.Common
  - Agda.Compiler.JS
    - Agda.Compiler.JS.Compiler
    - Agda.Compiler.JS.Pretty
    - Agda.Compiler.JS.Substitution
    - Agda.Compiler.JS.Syntax
  - Agda.Compiler.MAlonzo
    - Agda.Compiler.MAlonzo.Coerce
    - Agda.Compiler.MAlonzo.Compiler
    - Agda.Compiler.MAlonzo.Encode
    - Agda.Compiler.MAlonzo.HaskellTypes
    - Agda.Compiler.MAlonzo.Misc
    - Agda.Compiler.MAlonzo.Pragmas
    - Agda.Compiler.MAlonzo.Pretty
    - Agda.Compiler.MAlonzo.Primitives
    - Agda.Compiler.MAlonzo.Strict
  - 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.Library.Base
    - Agda.Interaction.Library.Parse
  - Agda.Interaction.MakeCase
  - Agda.Interaction.Monad
  - Agda.Interaction.Options
    - Agda.Interaction.Options.Help
    - Agda.Interaction.Options.Lenses
    - Agda.Interaction.Options.Warnings
  - Agda.Interaction.Response
  - Agda.Interaction.SearchAbout
- Agda.Main
- Agda.Syntax
  - Agda.Syntax.Abstract
    - Agda.Syntax.Abstract.Name
    - Agda.Syntax.Abstract.Pattern
    - Agda.Syntax.Abstract.PatternSynonyms
    - Agda.Syntax.Abstract.Pretty
    - Agda.Syntax.Abstract.UsedNames
    - Agda.Syntax.Abstract.Views
  - Agda.Syntax.Builtin
  - Agda.Syntax.Common
    - Agda.Syntax.Common.Aspect
    - Agda.Syntax.Common.Pretty
      - Agda.Syntax.Common.Pretty.ANSI
  - Agda.Syntax.Concrete
    - Agda.Syntax.Concrete.Attribute
    - Agda.Syntax.Concrete.Definitions
      - Agda.Syntax.Concrete.Definitions.Errors
      - Agda.Syntax.Concrete.Definitions.Monad
      - Agda.Syntax.Concrete.Definitions.Types
    - Agda.Syntax.Concrete.Fixity
    - Agda.Syntax.Concrete.Generic
    - Agda.Syntax.Concrete.Glyph
    - Agda.Syntax.Concrete.Name
    - Agda.Syntax.Concrete.Operators
      - Agda.Syntax.Concrete.Operators.Parser
        Agda.Syntax.Concrete.Operators.Parser.Monad
    - Agda.Syntax.Concrete.Pattern
    - Agda.Syntax.Concrete.Pretty
  - Agda.Syntax.DoNotation
  - Agda.Syntax.Fixity
  - Agda.Syntax.IdiomBrackets
  - Agda.Syntax.Info
  - Agda.Syntax.Internal
    - Agda.Syntax.Internal.Blockers
    - Agda.Syntax.Internal.Defs
    - Agda.Syntax.Internal.Elim
    - Agda.Syntax.Internal.Generic
    - Agda.Syntax.Internal.MetaVars
    - Agda.Syntax.Internal.Names
    - Agda.Syntax.Internal.Pattern
    - Agda.Syntax.Internal.SanityCheck
    - Agda.Syntax.Internal.Univ
  - 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.Scope.Base
    - Agda.Syntax.Scope.Flat
    - Agda.Syntax.Scope.Monad
  - Agda.Syntax.TopLevelModuleName
    - Agda.Syntax.TopLevelModuleName.Boot
  - Agda.Syntax.Translation
    - Agda.Syntax.Translation.AbstractToConcrete
    - Agda.Syntax.Translation.ConcreteToAbstract
    - Agda.Syntax.Translation.InternalToAbstract
    - Agda.Syntax.Translation.ReflectedToAbstract
  - Agda.Syntax.Treeless
- Agda.Termination
  - Agda.Termination.CallGraph
  - Agda.Termination.CallMatrix
  - Agda.Termination.CutOff
  - Agda.Termination.Monad
  - Agda.Termination.Order
  - Agda.Termination.RecCheck
  - Agda.Termination.Semiring
  - Agda.Termination.SparseMatrix
  - Agda.Termination.TermCheck
  - Agda.Termination.Termination
- Agda.TheTypeChecker
- Agda.TypeChecking
  - Agda.TypeChecking.Abstract
  - Agda.TypeChecking.CheckInternal
  - Agda.TypeChecking.CompiledClause
    - Agda.TypeChecking.CompiledClause.Compile
    - Agda.TypeChecking.CompiledClause.Match
  - Agda.TypeChecking.Constraints
  - Agda.TypeChecking.Conversion
    - Agda.TypeChecking.Conversion.Pure
  - Agda.TypeChecking.Coverage
    - Agda.TypeChecking.Coverage.Cubical
    - Agda.TypeChecking.Coverage.Match
    - Agda.TypeChecking.Coverage.SplitClause
    - Agda.TypeChecking.Coverage.SplitTree
  - Agda.TypeChecking.Datatypes
  - Agda.TypeChecking.DeadCode
  - Agda.TypeChecking.DisplayForm
  - Agda.TypeChecking.DropArgs
  - Agda.TypeChecking.Empty
  - Agda.TypeChecking.Errors
  - Agda.TypeChecking.EtaContract
  - Agda.TypeChecking.Forcing
  - Agda.TypeChecking.Free
    - Agda.TypeChecking.Free.Lazy
    - Agda.TypeChecking.Free.Precompute
    - Agda.TypeChecking.Free.Reduce
  - 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.Level.Solve
  - Agda.TypeChecking.LevelConstraints
  - Agda.TypeChecking.Lock
  - Agda.TypeChecking.MetaVars
    - Agda.TypeChecking.MetaVars.Mention
    - Agda.TypeChecking.MetaVars.Occurs
  - Agda.TypeChecking.Modalities
  - Agda.TypeChecking.Monad
    - Agda.TypeChecking.Monad.Base
      - Agda.TypeChecking.Monad.Base.Warning
    - 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.Modality
    - 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.Opacity
  - Agda.TypeChecking.Patterns
    - Agda.TypeChecking.Patterns.Abstract
    - Agda.TypeChecking.Patterns.Internal
    - Agda.TypeChecking.Patterns.Match
  - Agda.TypeChecking.Polarity
  - Agda.TypeChecking.Positivity
    - Agda.TypeChecking.Positivity.Occurrence
  - Agda.TypeChecking.Pretty
    - Agda.TypeChecking.Pretty.Call
    - Agda.TypeChecking.Pretty.Constraint
    - Agda.TypeChecking.Pretty.Warning
  - Agda.TypeChecking.Primitive
    - Agda.TypeChecking.Primitive.Base
    - Agda.TypeChecking.Primitive.Cubical
      - Agda.TypeChecking.Primitive.Cubical.Base
      - Agda.TypeChecking.Primitive.Cubical.Glue
      - Agda.TypeChecking.Primitive.Cubical.HCompU
      - Agda.TypeChecking.Primitive.Cubical.Id
  - Agda.TypeChecking.ProjectionLike
  - Agda.TypeChecking.Quote
  - Agda.TypeChecking.ReconstructParameters
  - Agda.TypeChecking.RecordPatterns
  - Agda.TypeChecking.Records
  - Agda.TypeChecking.Reduce
    - Agda.TypeChecking.Reduce.Fast
    - Agda.TypeChecking.Reduce.Monad
  - Agda.TypeChecking.Rewriting
    - Agda.TypeChecking.Rewriting.Clause
    - Agda.TypeChecking.Rewriting.Confluence
    - Agda.TypeChecking.Rewriting.NonLinMatch
    - Agda.TypeChecking.Rewriting.NonLinPattern
  - Agda.TypeChecking.Rules
    - Agda.TypeChecking.Rules.Application
    - Agda.TypeChecking.Rules.Builtin
      - Agda.TypeChecking.Rules.Builtin.Coinduction
    - 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.Unify
        Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
        
        Agda.TypeChecking.Rules.LHS.Unify.Types
    - Agda.TypeChecking.Rules.Record
    - Agda.TypeChecking.Rules.Term
  - Agda.TypeChecking.Serialise
    - 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.Serialise.Instances.Internal
  - Agda.TypeChecking.SizedTypes
    - Agda.TypeChecking.SizedTypes.Solve
    - Agda.TypeChecking.SizedTypes.Syntax
    - Agda.TypeChecking.SizedTypes.Utils
    - Agda.TypeChecking.SizedTypes.WarshallSolver
  - Agda.TypeChecking.Sort
  - Agda.TypeChecking.Substitute
    - Agda.TypeChecking.Substitute.Class
    - Agda.TypeChecking.Substitute.DeBruijn
  - Agda.TypeChecking.SyntacticEquality
  - Agda.TypeChecking.Telescope
    - Agda.TypeChecking.Telescope.Path
  - 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.BoolSet
  - Agda.Utils.Boolean
  - 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.AdjacencyMap.Unidirectional
    - Agda.Utils.Graph.TopSort
  - Agda.Utils.Hash
  - Agda.Utils.HashTable
  - Agda.Utils.Haskell
    - Agda.Utils.Haskell.Syntax
  - Agda.Utils.IO
    - Agda.Utils.IO.Binary
    - Agda.Utils.IO.Directory
    - Agda.Utils.IO.TempFile
    - Agda.Utils.IO.UTF8
  - Agda.Utils.IORef
  - Agda.Utils.Impossible
  - Agda.Utils.IndexedList
  - Agda.Utils.IntSet
    - Agda.Utils.IntSet.Infinite
  - Agda.Utils.Lens
    - Agda.Utils.Lens.Examples
  - Agda.Utils.List
  - Agda.Utils.List1
  - Agda.Utils.List2
  - Agda.Utils.ListT
  - Agda.Utils.Map
  - Agda.Utils.Maybe
    - Agda.Utils.Maybe.Strict
  - Agda.Utils.Memo
  - Agda.Utils.Monad
  - Agda.Utils.Monoid
  - Agda.Utils.Null
  - Agda.Utils.POMonoid
  - Agda.Utils.Parser
    - Agda.Utils.Parser.MemoisedCPS
  - Agda.Utils.PartialOrd
  - Agda.Utils.Permutation
  - Agda.Utils.Pointer
  - Agda.Utils.ProfileOptions
  - 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 45 packages(full list with versions):

aeson, Agda, ansi-terminal, array, async, base, binary, blaze-html, boxes, bytestring, case-insensitive, containers, data-hash, deepseq, directory, dlist, edit-distance, equivalence, exceptions, filepath, ghc-compact, gitrev, hashable, haskeline, monad-control, mtl, murmur-hash, parallel, peano, pretty, process, regex-tdfa, split, stm, STMonadTrans, strict, text, time, time-compat, transformers, and many more

Used by 1 package in nightly-2024-01-16(full list with versions):

Agda

Agda 2

The official Agda logo

Note that this README is only about Agda, not its standard library. See the Agda Wiki for information about the library.

Documentation

User manual (per-commit pdf can be downloaded from the github actions page)
CHANGELOG

Getting Started

Contributing to Agda

Contribution how-to: HACKING
Haskell style-guide

Changes

Release notes for Agda version 2.6.4.1

This is a minor release of Agda 2.6.4 featuring a few changes:

Make recursion on proofs legal again.
Improve performance, e.g. by removing debug printing unless built with cabal flag debug.
Switch to XDG directory convention.
Reflection: change to order of results returned by getInstances.
Fix some internal errors.

Installation

Agda supports GHC versions 8.6.5 to 9.8.1.
Verbose output printing via -v or --verbose is now only active if Agda is built with the debug cabal flag. Without debug, no code is generated for verbose printing, which makes building Agda faster and Agda itself faster as well. (PR #6863)

Language

A change in 2.6.4 that prevented all recursion on proofs, i.e., members of a type A : Prop ℓ, has been reverted. It is possible again to use proofs as termination arguments. (See issue #6930.)

Reflection

Changes to the meta-programming facilities.

The reflection primitive getInstances will now return instance candidates ordered by specificity, rather than in unspecified order: If a candidate c1 : T has a type which is a substitution instance of that of another candidate c2 : S, c1 will appear earlier in the list.

As a concrete example, if you have instances F (Nat → Nat), F (Nat → a), and F (a → b), they will be returned in this order. See issue #6944 for further motivation.

Library management

Agda now follows the XDG base directory standard on Unix-like systems, see PR #6858. This means, it will look for configuration files in ~/.config/agda rather than ~/.agda.

For backward compatibility, if you still have an ~/.agda directory, it will look there first.

No change on Windows, it will continue to use %APPDATA% (e.g. C:/Users/USERNAME/AppData/Roaming/agda).

Other issues closed

For 2.6.4.1, the following issues were also closed (see bug tracker):

#6745: Strange interaction between opaque and let open
#6746: Support GHC 9.8
#6852: Follow XDG Base Directory Specification
#6913: Internal error on primLockUniv-sorted functions
#6930: Termination checking with –prop: change in 2.6.4 compared with 2.6.3
#6931: Internal error with an empty parametrized module from a different file
#6941: Interaction between opaque and instance arguments
#6944: Order instances by specificity for reflection
#6953: Emacs 30 breaks agda mode
#6957: Agda stdlib installation instructions broken link
#6959: Warn about opaque unquoteDecl/unquoteDef
#6983: Refine command does not work on Emacs 30