The latest version of Agda is 2.7.0.1-0.
lib:Agda
Modules
- Agda.Auto.Auto
- Agda.Auto.CaseSplit
- Agda.Auto.Convert
- Agda.Auto.NarrowingSearch
- Agda.Auto.SearchControl
- Agda.Auto.Syntax
- Agda.Auto.Typecheck
- Agda.Benchmarking
- Agda.Compiler.CallCompiler
- 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.Case
- Agda.Compiler.JS.Compiler
- Agda.Compiler.JS.Parser
- Agda.Compiler.JS.Pretty
- Agda.Compiler.JS.Substitution
- Agda.Compiler.JS.Syntax
- Agda.Compiler.MAlonzo.Compiler
- Agda.Compiler.MAlonzo.Encode
- Agda.Compiler.MAlonzo.Misc
- Agda.Compiler.MAlonzo.Pretty
- Agda.Compiler.MAlonzo.Primitives
- Agda.ImpossibleTest
- Agda.Interaction.BasicOps
- Agda.Interaction.CommandLine
- Agda.Interaction.EmacsCommand
- Agda.Interaction.EmacsTop
- Agda.Interaction.Exceptions
- Agda.Interaction.FindFile
- Agda.Interaction.Highlighting.Dot
- Agda.Interaction.Highlighting.Emacs
- Agda.Interaction.Highlighting.Generate
- Agda.Interaction.Highlighting.HTML
- Agda.Interaction.Highlighting.LaTeX
- Agda.Interaction.Highlighting.Precise
- Agda.Interaction.Highlighting.Range
- Agda.Interaction.Highlighting.Vim
- Agda.Interaction.Imports
- Agda.Interaction.InteractionTop
- Agda.Interaction.MakeCase
- Agda.Interaction.Monad
- Agda.Interaction.Options
- Agda.Interaction.Options.Lenses
- Agda.Interaction.Response
- Agda.Main
- Agda.Syntax.Abstract
- Agda.Syntax.Abstract.Copatterns
- 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.Generic
- 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.Defs
- Agda.Syntax.Internal.Generic
- Agda.Syntax.Internal.Pattern
- 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.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.Translation.AbstractToConcrete
- Agda.Syntax.Translation.ConcreteToAbstract
- Agda.Syntax.Translation.InternalToAbstract
- Agda.Termination.CallGraph
- Agda.Termination.CallMatrix
- Agda.Termination.CutOff
- Agda.Termination.Inlining
- Agda.Termination.Monad
- Agda.Termination.Order
- Agda.Termination.RecCheck
- Agda.Termination.Semiring
- Agda.Termination.SparseMatrix
- Agda.Termination.TermCheck
- Agda.Termination.Termination
- Agda.Tests
- Agda.TheTypeChecker
- 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.Coverage
- Agda.TypeChecking.Coverage.Match
- Agda.TypeChecking.Coverage.SplitTree
- 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.Free.Lazy
- Agda.TypeChecking.Free.Old
- Agda.TypeChecking.Free.Tests
- Agda.TypeChecking.Implicit
- Agda.TypeChecking.Injectivity
- Agda.TypeChecking.InstanceArguments
- Agda.TypeChecking.Irrelevance
- Agda.TypeChecking.Level
- Agda.TypeChecking.LevelConstraints
- Agda.TypeChecking.MetaVars
- Agda.TypeChecking.MetaVars.Mention
- Agda.TypeChecking.MetaVars.Occurs
- 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.Abstract
- Agda.TypeChecking.Patterns.Match
- Agda.TypeChecking.Polarity
- Agda.TypeChecking.Positivity
- Agda.TypeChecking.Positivity.Occurrence
- Agda.TypeChecking.Positivity.Tests
- Agda.TypeChecking.Pretty
- Agda.TypeChecking.Primitive
- Agda.TypeChecking.ProjectionLike
- Agda.TypeChecking.Quote
- Agda.TypeChecking.RecordPatterns
- Agda.TypeChecking.Records
- Agda.TypeChecking.Reduce
- Agda.TypeChecking.Reduce.Monad
- Agda.TypeChecking.Rewriting
- Agda.TypeChecking.Rewriting.NonLinMatch
- Agda.TypeChecking.Rules.Builtin
- Agda.TypeChecking.Rules.Builtin.Coinduction
- 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.ProblemRest
- 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.SizedTypes.Solve
- Agda.TypeChecking.SizedTypes.Syntax
- Agda.TypeChecking.SizedTypes.Tests
- Agda.TypeChecking.SizedTypes.Utils
- Agda.TypeChecking.SizedTypes.WarshallSolver
- Agda.TypeChecking.Substitute
- Agda.TypeChecking.SyntacticEquality
- Agda.TypeChecking.Telescope
- Agda.TypeChecking.Test.Generators
- Agda.TypeChecking.Tests
- Agda.TypeChecking.Unquote
- Agda.TypeChecking.With
- 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.AdjacencyMap.Unidirectional
- Agda.Utils.Graph.AdjacencyMap.Unidirectional.Tests
- Agda.Utils.Hash
- Agda.Utils.HashMap
- Agda.Utils.IO.Binary
- Agda.Utils.IO.UTF8
- Agda.Utils.IORef
- Agda.Utils.Impossible
- Agda.Utils.Lens
- Agda.Utils.Lens.Examples
- Agda.Utils.List
- Agda.Utils.ListT
- Agda.Utils.ListT.Tests
- Agda.Utils.Map
- Agda.Utils.Maybe
- Agda.Utils.Maybe.Strict
- Agda.Utils.Monad
- Agda.Utils.Null
- Agda.Utils.PartialOrd
- Agda.Utils.Permutation
- Agda.Utils.Permutation.Tests
- 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
Dependencies
- QuickCheck lib:QuickCheck >=2.8 && <2.9
- Win32 lib:Win32 >=2.2 && <2.4
- array lib:array >=0.4.0.1 && <0.6
- base lib:base >=4.6.0.1 && <4.9
- base-orphans lib:base-orphans >=0.3.1 && <0.5
- binary lib:binary >=0.7.2.1 && <0.8
- boxes lib:boxes >=0.1.3 && <0.2
- bytestring lib:bytestring >=0.10.0.2 && <0.11
- containers lib:containers >=0.5.0.0 && <0.6
- data-hash lib:data-hash >=0.2.0.0 && <0.3
- deepseq lib:deepseq >=1.3.0.1 && <1.5
- directory lib:directory >=1.2.0.1 && <1.3
- edit-distance lib:edit-distance >=0.2.1.2 && <0.3
- equivalence lib:equivalence >=0.2.5 && <0.4
- filepath lib:filepath >=1.3.0.1 && <1.5
- geniplate-mirror lib:geniplate-mirror >=0.6.0.6 && <0.8
- hashable lib:hashable >=1.2.1.0 && <1.3
- hashtables lib:hashtables >=1.0.1.8 && <1.2 || >=1.2.0.2 && <1.3
- haskeline lib:haskeline >=0.7.1.3 && <0.8
- haskell-src-exts lib:haskell-src-exts >=1.16.0.1 && <1.17
- mtl lib:mtl >=2.1.1 && <=2.1.3.1 || >=2.2.1 && <2.3
- parallel lib:parallel >=3.2.0.4 && <3.3
- pretty lib:pretty >=1.1.1.0 && <1.1.1.2 || >=1.1.2 && <1.2
- process lib:process >=1.1.0.2 && <1.3
- strict lib:strict >=0.3.2 && <0.4
- template-haskell lib:template-haskell >=2.8.0.0 && <2.11
- text lib:text >=0.11.3.1 && <1.3
- time lib:time >=1.4.0.1 && <1.6
- transformers lib:transformers >=0.3 && <0.4 || >=0.4.1.0 && <0.5
- transformers-compat lib:transformers-compat >=0.3.3.3 && <0.5
- unordered-containers lib:unordered-containers >=0.2.5.0 && <0.2.6
- xhtml lib:xhtml >=3000.2.1 && <3000.3
- zlib lib:zlib >=0.4.0.1 && <0.6.1
Reverse dependencies
Direct only. Not exhaustive.
- Agda exe:agda
- acme-everything lib:acme-everything
- activehs exe:activehs
- agda-server exe:agda-server
- agda-snippets exe:agda-snippets
- agda-snippets lib:agda-snippets
- hakyll-agda lib:hakyll-agda
- lhs2TeX-hl exe:lhs2TeX-hl