Agda
latest
  • 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?
    • Prerequisites
    • Installation
    • ‘Hello world’ in Agda
    • Quick Guide to Editing, Type Checking and Compiling Agda Code
    • A List of Tutorials
  • Language Reference
    • Abstract definitions
    • Built-ins
    • Coinduction
    • Copatterns
    • Core language
    • 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
    • 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–2020 remains with the authors. Revision ef576672.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
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.