Welcome to Agda’s documentation!

• Overview
• Getting Started
  • What is Agda?
  • Installation
  • ‘Hello world’ in Agda
  • A Taste of Agda
  • A List of Tutorials
• 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 Type Theory
  • Implicit Arguments
  • Instance Arguments
  • Irrelevance
  • Lambda Abstraction
  • Local Definitions: let and where
  • Lexical Structure
  • Literal Overloading
  • Lossy Unification
  • Mixfix Operators
  • Modalities
  • Module System
  • Mutual Recursion
  • Opaque definitions
  • Pattern Synonyms
  • Polarity Annotations
  • 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
  • Automatic Proof Search (Auto)
  • Command-line options
  • Compilers
  • Emacs Mode
  • Literate Programming
  • Generating HTML
  • Generating LaTeX
  • Interface files
  • Library Management
  • Performance debugging
  • Search Definitions in Scope
• Contribute
  • Documentation
• The Agda Team and License

Indices and tables

• Index

• Search Page