Agda
latest
  • Overview
  • Getting Started
  • Language Reference
  • 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
  • The Agda Team and License
Agda
  • Tools

Tools¶

  • Automatic Proof Search (Auto)
    • Usage
    • Limitations
    • User feedback
  • Command-line options
    • Command-line options
    • Command-line and pragma options
    • Examples
    • Consistency checking of options used
  • Compilers
    • Backends
    • Optimizations
  • Emacs Mode
    • Menus
    • Configuration
    • Keybindings
    • Unicode input
    • Background highlighting
  • Literate Programming
    • Literate TeX
    • Literate reStructuredText
    • Literate Markdown
    • Literate Org
  • Generating HTML
    • Options
  • Generating LaTeX
    • Known pitfalls and issues
    • Options
    • Quicker generation without typechecking
    • Features
    • Examples
  • Interface files
    • Storage
    • Compilation
  • Library Management
    • Example: Using the standard library
    • Library files
    • The .agda-lib files associated to a given Agda file
    • Installing libraries
    • Using a library
    • Default libraries
    • Version numbers
    • Upgrading
  • Performance debugging
    • Measuring typechecking performance
    • Measuring run-time performance
  • Search Definitions in Scope
    • Usage
Previous Next

© Copyright 2005–2023 remains with the authors.. Revision f8f97783.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
v2.6.3
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
nightly
Downloads
pdf
html
epub
On Read the Docs
Project Home
Builds