TOC

The Agda Reference Manual

Lexical Matters

1. Source Files
2. Comments
3. Literals
4. Names
5. Keywords (Hyperlinked Index)
6. Layout

Type Theory

1. Core Syntax
2. Typing Rules
3. Normalisation

Extended Syntax

1. Mixfix Operators
2. Fixity Declarations
3. Implicit Arguments
4. Instance Arguments
5. Pattern-matching Lambdas

Declarations

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

Modules

Further Topics

1. Totality
   1. Termination
   2. Positivity
   3. Guardedness
2. Universe Levels
3. Reflection
4. Relevance

Practical Matters

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

Standard Library