Agda
latest
  • Overview
  • Getting Started
  • Language Reference
  • Tools
  • Contribute
  • The Agda Team and License
Agda
  • Docs »
  • Welcome to Agda’s documentation!
  • Edit on GitHub

Welcome to Agda’s documentation!¶

  • Overview
  • Getting Started
    • Prerequisites
    • Installation
    • 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 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 Team and License

Indices and tables¶

  • Index
  • Search Page
Next

© Copyright 2005-2018 remains with the authors. Agda 2 was originally written by Ulf Norell, partially based on code from Agda 1 by Catarina Coquand and Makoto Takeyama, and from Agdalight by Ulf Norell and Andreas Abel. Agda 2 is currently actively developed mainly by Andreas Abel, Guillaume Allais, Jesper Cockx, Nils Anders Danielsson, Philipp Hausmann, Fredrik Nordvall Forsberg, Ulf Norell, Víctor López Juan, Andrés Sicard-Ramírez, and Andrea Vezzosi. Further, Agda 2 has received contributions by, amongst others, Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, Guillaume Brunerie, James Chapman, Dominique Devriese, Péter Diviánszki, Olle Fredriksson, Adam Gundry, Daniel Gustafsson, Kuen-Bang Hou (favonia), Patrik Jansson, Alan Jeffrey, Wolfram Kahl, Wen Kokke, John Leo, Fredrik Lindblad, Francesco Mazzoli, Stefan Monnier, Darin Morrison, Guilhem Moulin, Nicolas Pouillard, Benjamin Price, Nobuo Yamashita, Christian Sattler, Makoto Takeyama and Tesla Ice Zhang. The full list of contributors is available at https://github.com/agda/agda/graphs/contributors Revision c97a7abe.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
stable-2.5
issue-2153
Downloads
pdf
htmlzip
epub
On Read the Docs
Project Home
Builds

Free document hosting provided by Read the Docs.