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, Idris, Lean and NuPRL. This package includes both a command-line program (agda) and an Emacs mode. If you want to use the Emacs mode you can set it up by running agda-mode setup (see the README). Note that the Agda package does not follow the package versioning policy, because it is not intended to be used by third-party packages.


Keywords
mit, program, Propose Tags, Skip to Readme, , Index, Quick Jump, Agda.Auto.Auto, Agda.Auto.CaseSplit, Agda.Auto.Convert, Agda.Auto.NarrowingSearch, Agda.Auto.Options, Agda.Auto.SearchControl, Agda.Auto.Syntax, Agda.Auto.Typecheck, Agda.Benchmarking, Agda.Compiler.Backend, 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.Response, Agda.Interaction.SearchAbout, Agda.Main, 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.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.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.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.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.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.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.Update, Agda.Utils.VarSet, Agda.Utils.Warshall, Agda.Utils.WithDefault, Agda.Utils.Zipper, Agda.Version, Agda.VersionCommit, More info, Agda-2.6.4.3.tar.gz, browse, Package description, Package maintainers, AndreasAbel, AndresSicardRamirez, NilsAndersDanielsson, UlfNorell, edit package information , 2.6.2.0.20211129, 2.6.2.1, 2.6.2.1.20220320, 2.6.2.1.20220327, 2.6.2.2.20221106, 2.6.2.2.20221128, 2.6.2.2.20230105, 2.6.3.20230805, 2.6.3.20230914, 2.6.3.20230930, 2.6.4, 2.6.4.1, 2.6.4.2, 2.6.4.3, Agda Wiki, User manual, github actions, CHANGELOG, Installation, Quick guide to editing, type checking and compiling Agda code, HACKING, Haskell style-guide, agda, dependent-types, programming-language, proof-assistant, type-theory
License
MIT
Install
cabal install Agda-2.6.4.3

Documentation