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
  • Docs »
  • 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
    • Installing libraries
    • Using a library
    • Default libraries
    • Version numbers
    • Upgrading
  • Performance debugging
    • Measuring typechecking performance
    • Measuring run-time performance
  • Search Definitions in Scope
    • Usage
Next Previous

© Copyright 2005–2021 remains with the authors. Revision c880f861.

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