Tools

• Automatic Proof Search (Auto)
  • Usage
  • Limitations
  • User feedback
• Command-line options
  • Command-line options
  • Command-line and pragma options
• Compilers
  • Backends
  • Optimizations
• Emacs Mode
  • Keybindings
  • Unicode input
  • Highlight
• Literate Programming
  • Literate TeX
  • Literate reStructuredText
  • Literate Markdown
• Generating HTML
  • Options
• Generating LaTeX
  • Unicode and LaTeX
  • Features
  • Options
  • Counting Extended Grapheme Clusters
  • Quicker generation without typechecking
  • Known issues
  • Complete LaTeX Template for Literate Agda with Unicode
• Library Management
  • Example: Using the standard library
  • Library files
  • Installing libraries
  • Using a library
  • Default libraries
  • Version numbers
  • Upgrading