Command-line options

Command-line options

Agda accepts the following options.

General options

--version -V
Show version number
--help[=TOPIC] -?[TOPIC]
Show basically this help, or more help about TOPIC. Current topics available: warning.
--interactive -I
Start in interactive mode (no longer supported)
For use with the Emacs mode (no need to invoke yourself)
For use with other editors such as Atom (no need to invoke yourself)
Only scope-check the top-level module, do not type-check it


See Compilers for backend-specific options.

Do not treat the requested module as the main module of a program when compiling
Set DIR as directory for compiler output (default: the project root)
Disable the forcing optimisation
Set PATH as the executable to call to compile the backend’s output (default: ghc for the GHC backend).

Generating highlighted source code

Generate Vim highlighting files
Generate LaTeX with highlighted source code (see Generating LaTeX)
Set directory in which LaTeX files are placed to DIR (default: latex)
Count extended grapheme clusters when generating LaTeX code (see Counting Extended Grapheme Clusters)
Generate HTML files with highlighted source code (see Generating HTML)
Set directory in which HTML files are placed to DIR (default: html)
Set URL of the CSS file used by the HTML files to URL (can be relative)
Whether to highlight non-Agda code as comments in generated HTML files (default: all; see :ref: generating-html)
Generate a Dot file FILE with a module dependency graph

Imports and libraries

(see Library Management)

Ignore interface files (re-type check everything, except for builtin and primitive modules)
Ignore all interface files, including builtin and primitive modules; only use this if you know what you are doing!
Read and write interface files next to the Agda files they correspond to (i.e. do not attempt to regroup them in a _build/ directory at the project’s root).
--include-path=DIR -i=DIR
Look for imports in DIR
--library=DIR -l=LIB
Use library LIB
Use FILE instead of the standard libraries file
Don’t use any library files
Don’t use default library files

Command-line and pragma options

The following options can also be given in .agda files in the {-# OPTIONS --{opt₁} --{opt₂} ... #-} form at the top of the file.


Enable caching of typechecking (default)
Disable caching of typechecking

Printing and debugging

Show implicit arguments when printing
Show irrelevant arguments when printing
Don’t use unicode characters to print terms
--verbose=N -v=N
Set verbosity level to N

Copatterns and projections

Enable definitions by copattern matching (default; see Copatterns)
Disable definitions by copattern matching
Make postfix projection notation the default

Experimental features

Enable injective type constructors (makes Agda anti-classical and possibly inconsistent)
Enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) (see Irrelevance)
Enable declaration and use of REWRITE rules (see Rewriting)
Enable cubical features. Turns on --without-K (see Cubical)

Errors and warnings

Succeed and create interface file regardless of unsolved meta variables (see Metavariables)
Succeed and create interface file regardless of incomplete pattern-matching definitions
Do not warn about not strictly positive data types (see Positivity Checking)
Do not warn about possibly nonterminating code (see Termination Checking)
Set warning group or flag (see Warnings)

Pattern matching and equality

Disables definitions using Streicher’s K axiom (see Without K)
Overrides a global --without-K in a file (see Without K)
Disable pattern matching completely
Require all clauses in a definition to hold as definitional equalities unless marked CATCHALL (see Case trees)
Do not require all clauses in a definition to hold as definitional equalities (default)
Default records to no-eta-equality (see Eta-expansion)

Search depth and instances

Allow termination checker to count decrease/increase upto N (default: 1; see Termination Checking)
Set instance search depth to N (default: 500; see Instance Arguments)
Set maximum depth for pattern match inversion to N (default: 50). Should only be needed in pathological cases.
Don’t consider recursive instance arguments during pruning of instance candidates (default)
Consider recursive instance arguments during pruning of instance candidates

Other features

Disable postulates, unsafe OPTION pragmas and primTrustMe. Turns off --sized-types and --guardedness (at most one can be turned back on again) (see Safe Agda)
Ignore universe levels (this makes Agda inconsistent; see Universe Levels)
Enable typing rule Setω : Setω (this makes Agda inconsistent).
Enable sized types (default, inconsistent with constructor-based guarded corecursion; see Sized Types). Turned off by --safe (but can be turned on again, as long as not also --guardedness is on).
Disable sized types (see Sized Types)
Enable constructor-based guarded corecursion (default, inconsistent with sized types; see Coinduction). Turned off by --safe (but can be turned on again, as long as not also --sized-types is on).
Disable constructor-based guarded corecursion (see Coinduction)
Enable universe polymorphism (default; see Universe Levels)
Disable universe polymorphism (see Universe Levels)
Disable projection of irrelevant record fields (see Irrelevance)
Disable automatic compile-time inlining. Only definitions marked INLINE will be inlined.
Always expand Pattern Synonyms during printing. With this option enabled you can use pattern synonyms freely, but Agda will not use any pattern synonyms when printing goal types or error messages, or when generating patterns for case splits.
Enable double-checking of all terms using the internal typechecker
Disable the syntactic equality shortcut in the conversion checker
Disable reduction using the Agda Abstract Machine


The -W or --warning option can be used to disable or enable different warnings. The flag -W error (or --warning=error) can be used to turn all warnings into errors, while -W noerror turns this off again.

A group of warnings can be enabled by -W {group}, where group is one of the following:

All of the existing warnings
Default warning level
Ignore all warnings

Individual warnings can be turned on and off by -W {Name} and -W {noName} respectively. The flags available are:

RHS given despite an absurd pattern in the LHS.
Attempt to generalize over sort metas in ‘variable’ declaration.
Failed coverage checks.
Failed exact split checks.
Feature deprecation.
Empty abstract blocks.
Empty instance blocks.
Empty macro blocks.
Empty mutual blocks.
Empty postulate blocks.
Empty primitive blocks.
Empty private blocks.
Empty REWRITE pragmas.
Illformed as-clauses in import statements.
Instance arguments whose type does not end in a named or variable type are never considered by instance search.
Instance arguments with explicit arguments are never considered by instance search.
Instance declarations with explicit arguments are never considered by instance search.
CATCHALL pragmas before a non-function clause.
No positivity checking pragmas before non-data`, record or mutual blocks.
Termination checking pragmas before non-function or mutual blocks.
Inversions of pattern-matching failed due to exhausted inversion depth.
Unknown field in library file.
Names declared without an accompanying definition.
Names mentioned in an import statement which are not exported by the module in question.
Declarations not allowed in a mutual block.
Failed strict positivity checks.
Deprecated BUILTIN pragmas.
Multi-line comments spanning one or more literate text blocks.
Polarity pragmas for non-postulates.
COMPILE pragmas not allowed in safe mode.
COMPILE pragma targeting an erased symbol.
NO_TERMINATION_CHECK pragmas are deprecated.
Failed confluence checks while computing overlap.
Failed confluence checks while joining critical pairs.
NON_TERMINATING pragmas with the safe flag.
NO_POSITIVITY_CHECK pragmas with the safe flag.
NO_UNIVERSE_CHECK pragmas with the safe flag.
POLARITY pragmas with the safe flag.
postulate blocks with the safe flag
Unsafe OPTIONS pragmas with the safe flag.
TERMINATING pragmas with the safe flag.
primEraseEquality used with the safe and without-K flags.
Repeated variable name in telescope.
Failed termination checks.
Mixfix names without an associated fixity declaration.
Names not declared in the same scope as their syntax or fixity declaration.
Names not declared in the same scope as their polarity pragmas.
Unreachable function clauses.
Unsolved constraints.
Unsolved interaction meta variables.
Unsolved meta variables.
abstract blocks where they have no effect.
INLINE pragmas where they have no effect.
instance blocks where they have no effect.
private blocks where they have no effect.
public blocks where they have no effect.
primEraseEquality used with the without-K flags.
Terms marked as eligible for instance search should end with a name.
Importing a file not using e.g. --safe from one which does.
Importing a file using e.g. --cubical into one which doesn’t.

For example, the following command runs Agda with all warnings enabled, except for warnings about empty abstract blocks:

agda -W all --warning=noEmptyAbstract file.agda

Consistency checking of options used

Agda checks that options used in imported modules are consistent with each other.

An infective option is an option that if used in one module, must be used in all modules that depend on this module. The following options are infective:

  • --cubical
  • --prop

A coinfective option is an option that if used in one module, must be used in all modules that this module depends on. The following options are coinfective:

  • --safe
  • --without-K
  • --no-universe-polymorphism
  • --no-sized-types
  • --no-guardedness

Agda records the options used when generating an interface file. If any of the following options differ when trying to load the interface again, the source file is re-typechecked instead:

  • --termination-depth
  • --no-unicode
  • --allow-unsolved-metas
  • --allow-incomplete-matches
  • --no-positivity-check
  • --no-termination-check
  • --type-in-type
  • --omega-in-omega
  • --no-sized-types
  • --no-guardedness
  • --injective-type-constructors
  • --prop
  • --no-universe-polymorphism
  • --irrelevant-projections
  • --experimental-irrelevance
  • --without-K
  • --exact-split
  • --no-eta-equality
  • --rewriting
  • --cubical
  • --overlapping-instances
  • --safe
  • --double-check
  • --no-syntactic-equality
  • --no-auto-inline
  • --no-fast-reduce
  • --instance-search-depth
  • --inversion-max-depth
  • --warning