The Agda Reference Manual

Don't read this. Go here instead:

http://agda.readthedocs.org/en/latest

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. Implicit Arguments
4. Instance Arguments
5. Pattern-matching Lambdas

Declarations

1. Overview
2. Data
3. Records
4. Postulates
5. Functions
6. Pattern Matching

Modules

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

Further Topics

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

Practical Matters

1. Pragmas
2. Compilation
3. Foreign Function Interface
4. Literate Agda
5. Troubleshooting

Standard Library

OLD MATERIAL BELOW

The manual was reorganized at some point. Below is the old structure. Some links may point to the same pages as above. Some may not.

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

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