The Agda Reference Manual

We are currently updating the manual and moving material from the old outdated version to the new structure. Help with this process is welcomed. Also, if you notice errors in the manual, please fix them. Ask the community if you are unsure about something.

Lexical Matters

1. Source Files
2. Comments
3. Literals
4. Names
5. Keywords (A Useful Index to the Manual)
6. Layout

Syntax

1. Mixfix Operators
2. Fixity Declarations
3. Syntax Declarations
4. Inferred Terms
5. Implicit Arguments
6. Instance Arguments
   1. Modelling Type Classes with Instance Arguments
   2. Non-recursive Resolution for Instance Arguments
7. Pattern-matching Lambdas

Declarations

1. Data
2. Records
3. Postulates
4. Functions
5. Pattern Matching
6. Local Definitions
7. Primitive

Modules

1. Basics
2. Private definitions
3. Name modifiers
4. Re-exporting names
5. Parametrised Modules
6. Splitting a program over multiple files

Further Topics

1. Totality
2. Universe Polymorphism
3. Reflection
4. Irrelevance

Practical Matters

1. Emacs Interface
2. Goals
3. Pragmas
4. Auto
5. Compilation
6. Foreign Function Interface
7. Literate Agda
8. Troubleshooting

Standard Library

OLD MATERIAL BELOW

Introduction

1. What is Agda?
2. Structure of an Agda program

The language

1. Implicit arguments
   1. Finding the values of implicit arguments
2. Inductive data types and pattern matching
   1. Simple inductive types
   2. Parameterized inductive types
   3. Mutual inductive types
   4. Inductive families
   5. Inductive-recursive types
   6. Pattern matching
   7. with-expression
3. Ensuring totality
   1. Termination checker - algorithm description
4. Local definitions
5. Syntactic sugar
   1. Implicit arguments
   2. Mixfix notation
   3. With notation
6. Lexical matters
7. Coinductive data types
8. Reflection
9. Irrelevant fields and definitions
10. Pattern matching lambdas
11. Mutual definitions
12. Auto (agsy)

Using Agda

1. How to download/install the system
2. Emacs interface
   1. Agda mode key combinations
   2. How to input special characters
   3. How to see special characters
3. Command line invocation
4. Foreign function interface
5. Plugin
6. Literate Agda
7. Compiler

Libraries

1. The standard library

References

1. Bibliography

All reference manual related wiki pages enumerated below