Agda
v2.6.2.2
  • Overview
  • Getting Started
  • Language Reference
  • Tools
  • Contribute
  • The Agda Team and License
Agda
  • Docs »
  • Welcome to Agda’s documentation!

Welcome to Agda’s documentation!¶

The official Agda logo
  • 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
    • 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
    • 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
Next

© Copyright 2005–2022 remains with the authors. Revision 442c76ba.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: v2.6.2.2
Versions
latest
v2.6.2.2
v2.6.2.1
v2.6.2
v2.6.1.3
v2.6.1.2
v2.6.1.1
v2.6.1
v2.6.0.1
v2.6.0
v2.5.4.2
v2.5.4.1
v2.5.4
v2.5.3
v2.5.2
Downloads
pdf
html
epub
On Read the Docs
Project Home
Builds

Free document hosting provided by Read the Docs.