lib:Agda
Modules
- Agda.Benchmarking
- Agda.Compiler.Backend
- Agda.Compiler.Backend.Base
- Agda.Compiler.Builtin
- Agda.Compiler.CallCompiler
- Agda.Compiler.Common
- Agda.Compiler.JS.Compiler
- Agda.Compiler.JS.Pretty
- Agda.Compiler.JS.Substitution
- Agda.Compiler.JS.Syntax
- 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.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.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.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.Output
- Agda.Interaction.Response
- Agda.Interaction.Response.Base
- Agda.Interaction.SearchAbout
- Agda.Main
- Agda.Mimer.Mimer
- Agda.Mimer.Options
- 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.KeywordRange
- 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.Helpers
- 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.Base
- Agda.Syntax.Scope.Flat
- Agda.Syntax.Scope.Monad
- Agda.Syntax.TopLevelModuleName
- Agda.Syntax.TopLevelModuleName.Boot
- Agda.Syntax.Translation.AbstractToConcrete
- Agda.Syntax.Translation.ConcreteToAbstract
- Agda.Syntax.Translation.InternalToAbstract
- Agda.Syntax.Translation.ReflectedToAbstract
- Agda.Syntax.Treeless
- 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.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.DiscrimTree
- Agda.TypeChecking.DiscrimTree.Types
- 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.Types
- 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.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.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.Pretty
- 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.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.AdjacencyMap.Unidirectional
- Agda.Utils.Graph.TopSort
- Agda.Utils.Hash
- Agda.Utils.HashTable
- Agda.Utils.Haskell.Syntax
- Agda.Utils.IArray
- 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.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.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.Unsafe
- Agda.Utils.Update
- Agda.Utils.VarSet
- Agda.Utils.Warshall
- Agda.Utils.WithDefault
- Agda.Utils.Zipper
- Agda.Version
- Agda.VersionCommit
Dependencies
- STMonadTrans lib:STMonadTrans >=0.4.3 && <0.5
- Win32 lib:Win32 >=2.6.1.0 && <2.15
- aeson lib:aeson >=1.1.2.0 && <2.3
- ansi-terminal lib:ansi-terminal >=0.9 && <1.2
- array lib:array >=0.5.2.0 && <0.6
- async lib:async >=2.2 && <2.3
- base lib:base >=4.12.0.0 && <4.21
- binary lib:binary >=0.8.6.0 && <0.9
- blaze-html lib:blaze-html >=0.8 && <0.10
- boxes lib:boxes >=0.1.3 && <0.2
- bytestring lib:bytestring >=0.10.8.2 && <0.13
- case-insensitive lib:case-insensitive >=1.2.0.4 && <1.3
- containers lib:containers >=0.6.0.1 && <0.8
- data-hash lib:data-hash >=0.2.0.0 && <0.3
- deepseq lib:deepseq >=1.4.4.0 && <1.6
- directory lib:directory >=1.3.3.0 && <1.4
- dlist lib:dlist >=0.8 && <1.1
- edit-distance lib:edit-distance >=0.2.1.2 && <0.3
- equivalence lib:equivalence >=0.3.2 && <0.5
- exceptions lib:exceptions >=0.8 && <0.11
- filepath lib:filepath >=1.4.2.1 && <1.6
- ghc-compact lib:ghc-compact >=0.1 && <0.2
- gitrev lib:gitrev >=1.3.1 && <2
- hashable lib:hashable >=1.2.1.0 && <1.6
- haskeline lib:haskeline >=0.7.4.3 && <0.9
- monad-control lib:monad-control >=1.0.1.0 && <1.1
- mtl lib:mtl >=2.2.2 && <2.4
- murmur-hash lib:murmur-hash >=0.1 && <0.2
- parallel lib:parallel >=3.2.2.0 && <3.3
- peano lib:peano >=0.1.0.1 && <0.2
- pqueue lib:pqueue >=1.4.1.2 && <1.6
- pretty lib:pretty >=1.1.3.3 && <1.2
- process lib:process >=1.6.3.0 && <1.7
- regex-tdfa lib:regex-tdfa >=1.3.1.0 && <1.4
- split lib:split >=0.2.0.0 && <0.3
- stm lib:stm >=2.4.4 && <2.6
- strict lib:strict >=0.4.0.1 && <0.6
- text lib:text >=1.2.3.1 && <2.2
- text-icu lib:text-icu >=0.7.1.0
- time lib:time >=1.9.2 && <1.15
- transformers lib:transformers >=0.5.5.0 && <0.7
- unordered-containers lib:unordered-containers >=0.2.9.0 && <0.3
- uri-encode lib:uri-encode >=1.5.0.4 && <1.6
- vector lib:vector >=0.12 && <0.14
- vector-hashtables lib:vector-hashtables >=0.1.1.1 && <0.2
- zlib lib:zlib >=0.6 && <0.8
Reverse dependencies
Direct only. Not exhaustive.
- acme-everything lib:acme-everything
- activehs exe:activehs
- agda-server exe:agda-server
- agda-snippets exe:agda-snippets
- hakyll-agda lib:hakyll-agda
- lhs2TeX-hl exe:lhs2TeX-hl