otty / apps
All apps/Agda

Agda

agda

A dependently typed functional programming language.

Runs as agda|macOS, Linux, Windows|agda.readthedocs.io
Open form in Otty otty.toml

Command form

ai-draft · 2 tasks · 13 fields

Type-check an Agda module with a few common options and optionally generate HTML, LaTeX or Vim highlighting. Compiler backends, interaction mode and the many pragma-style flags are left out.

Opens the form; the finished command lands at your prompt, unrun
Run in Otty
otty gui agda
Type-check an Agda fileExample values, fixed in this page — nothing here reaches a terminal
Basic
Agda file*
file
Safe mode
--safe
Import search directories
directory
Libraries
string
TasksEach one presets the form for one job
Type-check
filesafeinclude_pathlibrary
Generate HTML
filehtmlinclude_pathlibrary
ParametersOnly these flags are editable in the form
Agda file
path · positional 0
Safe mode
boolean
--safe
Without K
boolean
--without-K
Allow unsolved metas
boolean
--allow-unsolved-metas
Import search directories
path · repeatable
--include-path
Libraries
string · repeatable
--library
Libraries file
path
--library-file
Generate HTML
boolean
--html
Generate LaTeX
boolean
--latex
Generate Vim highlighting
boolean
--vim
Dependency graph (Dot file)
path
--dependency-graph
Only scope-check
boolean
--only-scope-checking
Ignore interface files
boolean
--ignore-interfaces
SourcesEvery flag above is checked against these
docs
--html Generate HTML files with highlighted source code --latex Generate LaTeX with highlighted source code --vim Generate Vim highlighting files. --include-path={DIR}, -i {DIR} Look for imports in DIR. This option can be given multiple times. --library={DIR}, -l {LIB} Use library LIB. --library-file={FILE} Use FILE instead of the standard libraries file. --…
manuallatest 2026-10

agda.readthedocs.io

Before it fills your prompt, Otty checks the installed agda against its version. A form that does not match your version is not offered.