The latest version of Agda is 2.7.0.1-2.
lib:Agda
Modules
- Agda.Compiler.Agate.Classify
- Agda.Compiler.Agate.Common
- Agda.Compiler.Agate.Main
- Agda.Compiler.Agate.OptimizedPrinter
- Agda.Compiler.Agate.TranslateName
- Agda.Compiler.Agate.UntypedPrinter
- Agda.Compiler.Alonzo.Haskell
- Agda.Compiler.Alonzo.Main
- Agda.Compiler.Alonzo.Names
- Agda.Compiler.Alonzo.PatternMonad
- Agda.Compiler.HaskellTypes
- Agda.Compiler.MAlonzo.Compiler
- Agda.Compiler.MAlonzo.Encode
- Agda.Compiler.MAlonzo.Misc
- Agda.Compiler.MAlonzo.Pretty
- Agda.Compiler.MAlonzo.Primitives
- Agda.Interaction.BasicOps
- Agda.Interaction.CommandLine.CommandLine
- Agda.Interaction.Exceptions
- Agda.Interaction.GhciTop
- Agda.Interaction.Highlighting.Emacs
- Agda.Interaction.Highlighting.Generate
- Agda.Interaction.Highlighting.HTML
- Agda.Interaction.Highlighting.Precise
- Agda.Interaction.Highlighting.Range
- Agda.Interaction.Highlighting.Vim
- Agda.Interaction.Imports
- Agda.Interaction.MakeCase
- Agda.Interaction.Monad
- Agda.Interaction.Options
- Agda.Main
- Agda.Syntax.Abstract
- Agda.Syntax.Abstract.Name
- Agda.Syntax.Abstract.Pretty
- Agda.Syntax.Abstract.Views
- Agda.Syntax.Common
- Agda.Syntax.Concrete
- Agda.Syntax.Concrete.Definitions
- Agda.Syntax.Concrete.Name
- Agda.Syntax.Concrete.Operators
- Agda.Syntax.Concrete.Operators.Parser
- Agda.Syntax.Concrete.Pretty
- Agda.Syntax.Fixity
- Agda.Syntax.Info
- Agda.Syntax.Internal
- Agda.Syntax.Internal.Generic
- Agda.Syntax.Internal.Pattern
- Agda.Syntax.Literal
- 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.LookAhead
- Agda.Syntax.Parser.Monad
- Agda.Syntax.Parser.Parser
- Agda.Syntax.Parser.StringLiterals
- Agda.Syntax.Parser.Tokens
- Agda.Syntax.Position
- Agda.Syntax.Scope.Base
- Agda.Syntax.Scope.Monad
- Agda.Syntax.Strict
- Agda.Syntax.Translation.AbstractToConcrete
- Agda.Syntax.Translation.ConcreteToAbstract
- Agda.Syntax.Translation.InternalToAbstract
- Agda.Termination.CallGraph
- Agda.Termination.Lexicographic
- Agda.Termination.Matrix
- Agda.Termination.Semiring
- Agda.Termination.TermCheck
- Agda.Termination.Termination
- Agda.Tests
- Agda.TypeChecker
- Agda.TypeChecking.Abstract
- Agda.TypeChecking.Constraints
- Agda.TypeChecking.Conversion
- Agda.TypeChecking.Coverage
- Agda.TypeChecking.Coverage.Match
- Agda.TypeChecking.DisplayForm
- Agda.TypeChecking.Empty
- Agda.TypeChecking.Errors
- Agda.TypeChecking.EtaContract
- Agda.TypeChecking.Free
- Agda.TypeChecking.Implicit
- Agda.TypeChecking.Injectivity
- Agda.TypeChecking.MetaVars
- Agda.TypeChecking.Monad
- Agda.TypeChecking.Monad.Base
- Agda.TypeChecking.Monad.Builtin
- Agda.TypeChecking.Monad.Closure
- Agda.TypeChecking.Monad.Constraints
- Agda.TypeChecking.Monad.Context
- Agda.TypeChecking.Monad.Debug
- 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.Signature
- Agda.TypeChecking.Monad.SizedTypes
- Agda.TypeChecking.Monad.State
- Agda.TypeChecking.Monad.Statistics
- Agda.TypeChecking.Monad.Trace
- Agda.TypeChecking.Patterns.Match
- Agda.TypeChecking.Polarity
- Agda.TypeChecking.Positivity
- Agda.TypeChecking.Pretty
- Agda.TypeChecking.Primitive
- Agda.TypeChecking.Rebind
- Agda.TypeChecking.Records
- Agda.TypeChecking.Reduce
- Agda.TypeChecking.Rules.Builtin
- Agda.TypeChecking.Rules.Data
- Agda.TypeChecking.Rules.Decl
- Agda.TypeChecking.Rules.Def
- Agda.TypeChecking.Rules.LHS
- Agda.TypeChecking.Rules.LHS.Implicit
- Agda.TypeChecking.Rules.LHS.Instantiate
- Agda.TypeChecking.Rules.LHS.Problem
- Agda.TypeChecking.Rules.LHS.Split
- Agda.TypeChecking.Rules.LHS.Unify
- Agda.TypeChecking.Rules.Record
- Agda.TypeChecking.Rules.Term
- Agda.TypeChecking.Serialise
- Agda.TypeChecking.SizedTypes
- Agda.TypeChecking.Substitute
- Agda.TypeChecking.Telescope
- Agda.TypeChecking.Test.Generators
- Agda.TypeChecking.Tests
- Agda.TypeChecking.With
- Agda.Utils.Char
- Agda.Utils.Either
- Agda.Utils.FileName
- Agda.Utils.Fresh
- Agda.Utils.Function
- Agda.Utils.Generics
- Agda.Utils.Graph
- Agda.Utils.Hash
- Agda.Utils.IO
- Agda.Utils.Impossible
- Agda.Utils.List
- Agda.Utils.Map
- Agda.Utils.Maybe
- Agda.Utils.Monad
- Agda.Utils.Monad.Undo
- Agda.Utils.Permutation
- Agda.Utils.Pointer
- Agda.Utils.Pretty
- Agda.Utils.QuickCheck
- Agda.Utils.ReadP
- Agda.Utils.SemiRing
- Agda.Utils.Serialise
- Agda.Utils.Size
- Agda.Utils.String
- Agda.Utils.Suffix
- Agda.Utils.TestHelpers
- Agda.Utils.Trace
- Agda.Utils.Trie
- Agda.Utils.Tuple
- Agda.Utils.Unicode
- Agda.Utils.Warshall
- Agda.Version
Dependencies
- QuickCheck lib:QuickCheck ==2.1.0.1
- array lib:array >=0.1 && <1
- base lib:base >=4.1 && <4.2
- binary lib:binary >=0.4.4 && <0.6
- bytestring lib:bytestring >=0.9.0.1 && <1
- containers lib:containers >=0.1.0 && <1
- directory lib:directory >=1 && <2
- filepath lib:filepath >=1.1 && <2
- ghc-prim lib:ghc-prim >=0.1 && <1
- haskeline lib:haskeline >=0.3 && <0.7
- haskell-src lib:haskell-src >=1.0.1.1 && <2
- haskell98 lib:haskell98 >=1.0.1 && <2
- mtl lib:mtl >=1.1 && <2
- old-time lib:old-time >=1 && <2
- pretty lib:pretty >=1 && <2
- process lib:process >=1.0.1.0 && <2
- syb lib:syb >=0.1 && <0.2
- utf8-string lib:utf8-string >=0.3 && <0.4
- xhtml lib:xhtml >=3000.2 && <3000.3
- zlib lib:zlib >=0.4.0.1 && <1
Reverse dependencies
Direct only. Not exhaustive.
- Agda-executable exe:agda
- acme-everything lib:acme-everything
- activehs exe:activehs
- agda-snippets exe:agda-snippets