Welcome to Agda’s documentation!¶
- Overview
- Getting Started
- Language Reference
- Abstract definitions
- Built-ins
- Coinduction
- Copatterns
- Core language
- Coverage Checking
- Cubical
- Cubical compatible
- Cumulativity
- Data Types
- Flat Modality
- Foreign Function Interface
- Function Definitions
- Function Types
- Generalization of Declared Variables
- Guarded Cubical
- Implicit Arguments
- Instance Arguments
- Irrelevance
- Lambda Abstraction
- Local Definitions: let and where
- Lexical Structure
- Literal Overloading
- Lossy Unification
- Mixfix Operators
- Module System
- Mutual Recursion
- Pattern Synonyms
- Positivity Checking
- Postulates
- Pragmas
- Prop
- Record Types
- Reflection
- Rewriting
- Run-time Irrelevance
- Safe Agda
- Sized Types
- Sort System
- Syntactic Sugar
- Syntax Declarations
- Telescopes
- Termination Checking
- Two-Level Type Theory
- Universe Levels
- With-Abstraction
- Without K
- Tools
- Contribute
- The Agda Team and License