Agda
A dependently typed functional programming language and proof assistant
https://wiki.portal.chalmers.se/agda/
Version on this page: | 2.6.4@rev:1 |
LTS Haskell 22.41: | 2.6.4.3@rev:1 |
Stackage Nightly 2024-11-10: | 2.7.0.1@rev:2 |
Latest on Hackage: | 2.7.0.1@rev:2 |
Maintained by The Agda Team
This version can be pinned in stack with:
Agda-2.6.4@sha256:298bc3b261ad034bf4ee788834a4d296aa5c2f6ea17ac4bef44e3daea53a7cd8,28443
Module documentation for 2.6.4
- 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.TopLevelModuleName
- 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.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.Modalities
- 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.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.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.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.TopSort
- Agda.Utils.Hash
- Agda.Utils.HashTable
- 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.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 lts-21.21(full list with versions):