Agda-2.2.10: A dependently typed functional programming language and proof assistantContentsIndex
Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda is a dependently typed functional programming language: It has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code).

Agda is also a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL.

Note that if you want to use the command-line program (agda), then you should also install the Agda-executable package. The Agda package includes an Emacs mode for Agda, but you need to set up the Emacs mode yourself (for instance by running agda-mode setup; see the README).

Note also that this library does not follow the package versioning policy, because the library is only intended to be used by the Emacs mode and the Agda-executable package.

Modules
show/hideAgda
show/hideAuto
Agda.Auto.Auto
Agda.Auto.CaseSplit
Agda.Auto.Convert
Agda.Auto.NarrowingSearch
Agda.Auto.SearchControl
Agda.Auto.Syntax
Agda.Auto.Typecheck
show/hideCompiler
show/hideEpic
Agda.Compiler.Epic.AuxAST
Agda.Compiler.Epic.CompileState
Agda.Compiler.Epic.Compiler
Agda.Compiler.Epic.ConstructorIrrelevancy
Agda.Compiler.Epic.Epic
Agda.Compiler.Epic.Erasure
Agda.Compiler.Epic.Forcing
Agda.Compiler.Epic.FromAgda
Agda.Compiler.Epic.LambdaLift
Agda.Compiler.Epic.NatDetection
Agda.Compiler.Epic.Primitive
Agda.Compiler.HaskellTypes
show/hideMAlonzo
Agda.Compiler.MAlonzo.Compiler
Agda.Compiler.MAlonzo.Encode
Agda.Compiler.MAlonzo.Misc
Agda.Compiler.MAlonzo.Pretty
Agda.Compiler.MAlonzo.Primitives
Agda.ImpossibleTest
show/hideInteraction
Agda.Interaction.BasicOps
show/hideCommandLine
Agda.Interaction.CommandLine.CommandLine
Agda.Interaction.Exceptions
Agda.Interaction.FindFile
Agda.Interaction.GhciTop
show/hideHighlighting
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
show/hidePackaging
Agda.Packaging.Config
Agda.Packaging.Database
Agda.Packaging.Monad
Agda.Packaging.Types
show/hideSyntax
show/hideAgda.Syntax.Abstract
Agda.Syntax.Abstract.Name
Agda.Syntax.Abstract.Pretty
Agda.Syntax.Abstract.Views
Agda.Syntax.Common
show/hideAgda.Syntax.Concrete
Agda.Syntax.Concrete.Definitions
Agda.Syntax.Concrete.Name
show/hideAgda.Syntax.Concrete.Operators
Agda.Syntax.Concrete.Operators.Parser
Agda.Syntax.Concrete.Pretty
Agda.Syntax.Fixity
Agda.Syntax.Info
show/hideAgda.Syntax.Internal
Agda.Syntax.Internal.Generic
Agda.Syntax.Internal.Pattern
Agda.Syntax.Literal
Agda.Syntax.Notation
show/hideAgda.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
show/hideScope
Agda.Syntax.Scope.Base
Agda.Syntax.Scope.Monad
Agda.Syntax.Strict
show/hideTranslation
Agda.Syntax.Translation.AbstractToConcrete
Agda.Syntax.Translation.ConcreteToAbstract
Agda.Syntax.Translation.InternalToAbstract
show/hideTermination
Agda.Termination.CallGraph
Agda.Termination.Lexicographic
Agda.Termination.Matrix
Agda.Termination.Semiring
Agda.Termination.SparseMatrix
Agda.Termination.TermCheck
Agda.Termination.Termination
Agda.Tests
Agda.TypeChecker
show/hideTypeChecking
Agda.TypeChecking.Abstract
show/hideAgda.TypeChecking.CompiledClause
Agda.TypeChecking.CompiledClause.Match
Agda.TypeChecking.Constraints
Agda.TypeChecking.Conversion
show/hideAgda.TypeChecking.Coverage
Agda.TypeChecking.Coverage.Match
Agda.TypeChecking.Datatypes
Agda.TypeChecking.DisplayForm
Agda.TypeChecking.Empty
Agda.TypeChecking.Errors
Agda.TypeChecking.EtaContract
Agda.TypeChecking.Forcing
Agda.TypeChecking.Free
Agda.TypeChecking.Implicit
Agda.TypeChecking.Injectivity
Agda.TypeChecking.Level
show/hideAgda.TypeChecking.MetaVars
Agda.TypeChecking.MetaVars.Occurs
show/hideAgda.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
show/hidePatterns
Agda.TypeChecking.Patterns.Match
Agda.TypeChecking.Polarity
Agda.TypeChecking.Positivity
Agda.TypeChecking.Pretty
Agda.TypeChecking.Primitive
Agda.TypeChecking.Quote
Agda.TypeChecking.Rebind
Agda.TypeChecking.RecordPatterns
Agda.TypeChecking.Records
Agda.TypeChecking.Reduce
show/hideRules
show/hideAgda.TypeChecking.Rules.Builtin
Agda.TypeChecking.Rules.Builtin.Coinduction
Agda.TypeChecking.Rules.Data
Agda.TypeChecking.Rules.Decl
Agda.TypeChecking.Rules.Def
show/hideAgda.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
show/hideTest
Agda.TypeChecking.Test.Generators
Agda.TypeChecking.Tests
Agda.TypeChecking.UniversePolymorphism
Agda.TypeChecking.With
show/hideUtils
Agda.Utils.Char
Agda.Utils.Either
Agda.Utils.FileName
Agda.Utils.Fresh
Agda.Utils.Function
Agda.Utils.Generics
Agda.Utils.Graph
Agda.Utils.Hash
show/hideIO
Agda.Utils.IO.Binary
Agda.Utils.IO.Locale
Agda.Utils.IO.UTF8
Agda.Utils.Impossible
Agda.Utils.List
Agda.Utils.Map
Agda.Utils.Maybe
Agda.Utils.Monad
Agda.Utils.Permutation
Agda.Utils.Pointer
Agda.Utils.Pretty
Agda.Utils.QuickCheck
Agda.Utils.ReadP
Agda.Utils.SemiRing
Agda.Utils.Size
Agda.Utils.String
Agda.Utils.Suffix
Agda.Utils.TestHelpers
Agda.Utils.Trie
Agda.Utils.Tuple
Agda.Utils.Unicode
Agda.Utils.Warshall
Agda.Version
Produced by Haddock version 2.6.1