Agda
A dependently typed functional programming language and proof assistant
http://wiki.portal.chalmers.se/agda/
Version on this page: | 2.4.2.5@rev:2 |
LTS Haskell 23.0: | 2.7.0.1@rev:2 |
Stackage Nightly 2024-12-09: | 2.7.0.1@rev:2 |
Latest on Hackage: | 2.7.0.1@rev:2 |
Maintained by Ulf Norell
This version can be pinned in stack with:
Agda-2.4.2.5@sha256:9c7786cfae8d92deb077650a31f41d15b8e1c8f15450419c268fd16162753515,21012
Module documentation for 2.4.2.5
- Agda
- Agda.Auto
- Agda.Benchmarking
- Agda.Compiler
- Agda.Compiler.CallCompiler
- Agda.Compiler.Epic
- Agda.Compiler.Epic.AuxAST
- Agda.Compiler.Epic.CaseOpts
- Agda.Compiler.Epic.CompileState
- Agda.Compiler.Epic.Compiler
- Agda.Compiler.Epic.Epic
- Agda.Compiler.Epic.Erasure
- Agda.Compiler.Epic.ForceConstrs
- Agda.Compiler.Epic.Forcing
- Agda.Compiler.Epic.FromAgda
- Agda.Compiler.Epic.Injection
- Agda.Compiler.Epic.Interface
- Agda.Compiler.Epic.NatDetection
- Agda.Compiler.Epic.Primitive
- Agda.Compiler.Epic.Smashing
- Agda.Compiler.Epic.Static
- Agda.Compiler.HaskellTypes
- Agda.Compiler.JS
- Agda.Compiler.MAlonzo
- Agda.ImpossibleTest
- Agda.Interaction
- Agda.Interaction.BasicOps
- Agda.Interaction.CommandLine
- Agda.Interaction.EmacsCommand
- Agda.Interaction.EmacsTop
- Agda.Interaction.Exceptions
- Agda.Interaction.FindFile
- Agda.Interaction.Highlighting
- Agda.Interaction.Imports
- Agda.Interaction.InteractionTop
- Agda.Interaction.MakeCase
- Agda.Interaction.Monad
- Agda.Interaction.Options
- Agda.Interaction.Response
- Agda.Main
- Agda.Syntax
- Agda.Syntax.Abstract
- Agda.Syntax.Common
- Agda.Syntax.Concrete
- Agda.Syntax.Fixity
- Agda.Syntax.Info
- Agda.Syntax.Internal
- Agda.Syntax.Literal
- Agda.Syntax.Notation
- Agda.Syntax.Parser
- Agda.Syntax.Position
- Agda.Syntax.Scope
- Agda.Syntax.Translation
- Agda.Termination
- Agda.Tests
- 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.DisplayForm
- Agda.TypeChecking.DropArgs
- Agda.TypeChecking.Empty
- Agda.TypeChecking.Errors
- Agda.TypeChecking.EtaContract
- Agda.TypeChecking.Forcing
- Agda.TypeChecking.Free
- Agda.TypeChecking.Implicit
- Agda.TypeChecking.Injectivity
- Agda.TypeChecking.InstanceArguments
- Agda.TypeChecking.Irrelevance
- Agda.TypeChecking.Level
- Agda.TypeChecking.LevelConstraints
- Agda.TypeChecking.MetaVars
- Agda.TypeChecking.Monad
- Agda.TypeChecking.Monad.Base
- Agda.TypeChecking.Monad.Benchmark
- Agda.TypeChecking.Monad.Builtin
- Agda.TypeChecking.Monad.Closure
- Agda.TypeChecking.Monad.Constraints
- Agda.TypeChecking.Monad.Context
- Agda.TypeChecking.Monad.Env
- Agda.TypeChecking.Monad.Exception
- Agda.TypeChecking.Monad.Imports
- Agda.TypeChecking.Monad.MetaVars
- Agda.TypeChecking.Monad.Mutual
- Agda.TypeChecking.Monad.Open
- Agda.TypeChecking.Monad.Options
- Agda.TypeChecking.Monad.Sharing
- Agda.TypeChecking.Monad.Signature
- Agda.TypeChecking.Monad.SizedTypes
- Agda.TypeChecking.Monad.State
- Agda.TypeChecking.Monad.Statistics
- Agda.TypeChecking.Monad.Trace
- Agda.TypeChecking.Patterns
- Agda.TypeChecking.Polarity
- Agda.TypeChecking.Positivity
- Agda.TypeChecking.Pretty
- Agda.TypeChecking.Primitive
- Agda.TypeChecking.ProjectionLike
- Agda.TypeChecking.Quote
- Agda.TypeChecking.RecordPatterns
- Agda.TypeChecking.Records
- Agda.TypeChecking.Reduce
- Agda.TypeChecking.Rewriting
- Agda.TypeChecking.Rules
- Agda.TypeChecking.Serialise
- Agda.TypeChecking.SizedTypes
- Agda.TypeChecking.Substitute
- Agda.TypeChecking.SyntacticEquality
- Agda.TypeChecking.Telescope
- Agda.TypeChecking.Test
- Agda.TypeChecking.Tests
- Agda.TypeChecking.Unquote
- Agda.TypeChecking.With
- Agda.Utils
- Agda.Utils.AssocList
- Agda.Utils.Bag
- Agda.Utils.Benchmark
- Agda.Utils.BiMap
- Agda.Utils.Char
- Agda.Utils.Cluster
- Agda.Utils.Either
- Agda.Utils.Empty
- Agda.Utils.Except
- Agda.Utils.Favorites
- Agda.Utils.FileName
- Agda.Utils.Function
- Agda.Utils.Functor
- Agda.Utils.Geniplate
- Agda.Utils.Graph
- Agda.Utils.Graph.AdjacencyMap
- Agda.Utils.Hash
- Agda.Utils.HashMap
- Agda.Utils.IO
- Agda.Utils.IORef
- Agda.Utils.Impossible
- Agda.Utils.Lens
- Agda.Utils.List
- Agda.Utils.ListT
- Agda.Utils.Map
- Agda.Utils.Maybe
- Agda.Utils.Monad
- Agda.Utils.Null
- Agda.Utils.PartialOrd
- Agda.Utils.Permutation
- Agda.Utils.Pointer
- Agda.Utils.Pretty
- Agda.Utils.QuickCheck
- Agda.Utils.ReadP
- Agda.Utils.SemiRing
- Agda.Utils.Singleton
- Agda.Utils.Size
- Agda.Utils.String
- Agda.Utils.Suffix
- Agda.Utils.TestHelpers
- Agda.Utils.Time
- Agda.Utils.Trie
- Agda.Utils.Tuple
- Agda.Utils.Update
- Agda.Utils.VarSet
- Agda.Utils.Warshall
- Agda.Version
Depends on 32 packages(full list with versions):
Agda, array, base, binary, boxes, bytestring, containers, data-hash, deepseq, directory, edit-distance, equivalence, filepath, geniplate-mirror, hashable, hashtables, haskeline, haskell-src-exts, mtl, parallel, pretty, process, QuickCheck, strict, template-haskell, text, time, transformers, transformers-compat, unordered-containers, xhtml, zlib
Used by 1 package in lts-3.22(full list with versions):