Welcome to Agda’s documentation!

• Overview
• Getting Started
  • Prerequisites
  • Installation
  • Quick Guide to Editing, Type Checking and Compiling Agda Code
• Language Reference
  • Abstract definitions
  • Built-ins
  • Coinduction
  • Copatterns
  • Core language
  • Cubical Type Theory in Agda
  • Data Types
  • Foreign Function Interface
  • Function Definitions
  • Function Types
  • Generalization of Declared Variables
  • Implicit Arguments
  • Instance Arguments
  • Irrelevance
  • Lambda Abstraction
  • Local Definitions: let and where
  • Lexical Structure
  • Literal Overloading
  • Mixfix Operators
  • Module System
  • Mutual Recursion
  • Pattern Synonyms
  • Positivity Checking
  • Postulates
  • Pragmas
  • Record Types
  • Reflection
  • Rewriting
  • Safe Agda
  • Sized Types
  • Syntactic Sugar
  • Syntax Declarations
  • Telescopes
  • Termination Checking
  • Universe Levels
  • With-Abstraction
  • Without K
• Tools
  • Automatic Proof Search (Auto)
  • Command-line options
  • Compilers
  • Emacs Mode
  • Literate Programming
  • Generating HTML
  • Generating LaTeX
  • Library Management
• Contribute
  • Documentation
• The Agda License
• The Agda Team

Indices and tables

• Index
• Search Page