Command-line options

Command-line options

Agda accepts the following options.

General options

--help[={TOPIC}], -?[{TOPIC}]

Show basically this help, or more help about TOPIC. Current topics available: warning.


For use with the Emacs mode (no need to invoke yourself).


New in version 2.6.1.

For use with other editors such as Atom (no need to invoke yourself).


New in version 2.6.3.

Makes Agda exit with a non-zero exit code if --interaction or --interaction-json are used and a type error is encountered. The option also makes Agda exit with exit code 113 if Agda fails to parse a command.

This option might for instance be used if Agda is controlled from a script.

--interactive, -I

Start in interactive mode (not maintained).


New in version 2.6.1.

Turn off the analysis whether a type signature likens that of a projection.

Projection-likeness is an optimization that reduces the size of terms by dropping parameter-like reconstructible function arguments. Thus, it is advisable to leave this optimization on, the flag is meant for debugging Agda.

See also the NOT_PROJECTION_LIKE pragma.


New in version 2.5.3.

Only scope-check the top-level module, do not type-check it (see Quicker generation without typechecking).

--version, -V

Show version number.


New in version 2.6.2.

Outputs the root (AGDA_DIR) of the directory structure holding Agda’s data files such as core libraries, style files for the backends etc.


New in version 2.6.3.

When writing to stdout or stderr Agda will (hopefully) replace code points that are not supported by the current locale or code page by something else, perhaps question marks.

This option is not supported when --interaction or --interaction-json are used, because when those options are used Agda uses UTF-8 when writing to stdout (and when reading from stdin).


See Compilers for backend-specific options.


Set DIR as directory for compiler output (default: the project root).


Do not treat the requested module as the main module of a program when compiling.


Set PATH as the executable to call to compile the backend’s output (default: ghc for the GHC backend).

Generating highlighted source code


New in version 2.5.3.

Count extended grapheme clusters when generating LaTeX code (see Counting Extended Grapheme Clusters). Available only when Agda was built with Cabal flag enable-cluster-counting.

Pragma option since 2.5.4.


Set URL of the CSS file used by the HTML files to URL (can be relative).


New in version 2.3.0.

Generate a Dot file FILE with a module dependency graph.


New in version 2.6.3.

Include modules from the given library in the dependency graph. This option can be used multiple times to include modules from several libraries. If this option is not used at all, then all modules are included. (Note that the module given on the command line might not be included.)

A module M is considered to be in the library L if L is the name of a .agda-lib file A associated to M (even if M’s file can not be found via the include paths in A).


New in version 2.2.0.

Generate HTML files with highlighted source code (see Generating HTML).


Set directory in which HTML files are placed to DIR (default: html).


New in version 2.6.0.

Whether to highlight non-Agda code as comments in generated HTML files (default: all; see Generating HTML).


New in version 2.3.2.

Generate LaTeX with highlighted source code (see Generating LaTeX).


New in version 2.5.2.

Set directory in which LaTeX files are placed to DIR (default: latex).


Generate Vim highlighting files.

Imports and libraries

(see Library Management)


New in version 2.6.0.

Ignore all interface files, including builtin and primitive modules; only use this if you know what you are doing!


Ignore interface files (re-type check everything, except for builtin and primitive modules).

--include-path={DIR}, -i={DIR}

Look for imports in DIR.

--library={DIR}, -l={LIB}

New in version 2.5.1.

Use library LIB.


New in version 2.5.1.

Use FILE instead of the standard libraries file.


New in version 2.6.1.

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).


New in version 2.5.1.

Don’t use default library files.


New in version 2.5.2.

Don’t use any library files.

Command-line and pragma options

The following options can also be given in .agda files using the OPTIONS pragma.


--caching, --no-caching

New in version 2.5.4.

Enable or disable caching of typechecking.

Default: --caching.

Printing and debugging


New in version 2.5.4.

Do not use unicode characters to print terms.


Show implicit arguments when printing.


New in version 2.3.2.

Show irrelevant arguments when printing.

--verbose={N}, -v={N}

Set verbosity level to N.


New in version 2.6.3.

Turn on profiling option PROF. Available options are


Measure time taken by various parts of the system (type checking, serialization, etc)


Measure time spent on individual (Agda) modules


Measure time spent on individual (Agda) definitions


Measure things related to sharing


Collect detailed statistics about serialization


Collect statistics about constraint solving


Count number of created metavariables


Measure time of interactive commands


Count number of times various steps of the conversion algorithm are used (reduction, eta-expansion, syntactic equality, etc)

Only one of internal, modules, and definitions can be turned on at a time. You can also give --profile=all to turn on all profiling options (choosing internal over modules and definitions, use --profile=modules --profile=all to pick modules instead).

Copatterns and projections

--copatterns, --no-copatterns

New in version 2.4.0.

Enable or disable definitions by copattern matching (see Copatterns).

Default: --copatterns (since


New in version 2.5.2.

Make postfix projection notation the default.

Experimental features


New in version 2.6.2.

Enable system calls during type checking (see Reflection).

--confluence-check, --local-confluence-check

New in version 2.6.1.

Enable optional (global or local) confluence checking of REWRITE rules (see Confluence checking).


New in version 2.6.0.

Enable cubical features. Turns on --cubical-compatible and --without-K (see Cubical).


New in version 2.6.3.

Enable a variant of Cubical Agda, and turn on --without-K.


New in version 2.3.0.

Enable potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) (see Irrelevance).


New in version 2.6.2.

Enable locks and ticks for guarded recursion (see Guarded Cubical Agda).


New in version 2.2.8.

Enable injective type constructors (makes Agda anti-classical and possibly inconsistent).

--prop, --no-prop

New in version 2.6.0.

Enable or disable declaration and use of definitionally proof-irrelevant propositions (see proof-irrelevant propositions).

Default: –no-prop.


New in version

Enable declaration and use of REWRITE rules (see Rewriting).


New in version 2.6.2.

Enable the use of strict (non-fibrant) type universes SSet (two-level type theory).

Errors and warnings


New in version 2.6.1.

Succeed and create interface file regardless of incomplete pattern-matching definitions. See also the NON_COVERING pragma.


Succeed and create interface file regardless of unsolved meta variables (see Metavariables).


Do not warn about not strictly positive data types (see Positivity Checking).


Do not warn about possibly nonterminating code (see Termination Checking).

--warning={GROUP|FLAG}, -W {GROUP|FLAG}

New in version 2.5.3.

Set warning group or flag (see Warnings).

Pattern matching and equality

--exact-split, --no-exact-split

New in version 2.5.1.

Require [do not require] all clauses in a definition to hold as definitional equalities unless marked CATCHALL (see Case trees).

Default: --no-exact-split.


New in version 2.5.1.

Default records to no-eta-equality (see Eta-expansion).


New in version 2.6.3.

Enable the cohesion modalities, in particular @♭ (see Flat Modality).


New in version 2.6.1.

Enable pattern matching on @♭ arguments (see Pattern Matching on @♭).


New in version 2.4.0.

Disable pattern matching completely.


New in version 2.4.2.

Overrides a global --without-K in a file (see Without K).


New in version 2.2.10.

Disables reasoning principles incompatible with univalent type theory, most importantly Streicher’s K axiom (see Without K).


New in version 2.6.3.

Generate internal support code necessary for use from Cubical Agda (see Cubical compatible). Implies --without-K.


New in version 2.6.1.

Prevent interactive case splitting from replacing variables with dot patterns (see Dot patterns).

Search depth and instances


New in version 2.5.2.

Set instance search depth to N (default: 500; see Instance Arguments).


New in version 2.5.4.

Set maximum depth for pattern match inversion to N (default: 50). Should only be needed in pathological cases.


New in version 2.2.8.

Allow termination checker to count decrease/increase upto N (default: 1; see Termination Checking).

--overlapping-instances, --no-overlapping-instances

New in version 2.6.0.

Consider [do not consider] recursive instance arguments during pruning of instance candidates.

Default: --no-overlapping-instances.

--qualified-instances, --no-qualified-instances

New in version 2.6.2.

Consider [do not consider] instances that are (only) in scope under a qualified name.

Default: --qualified-instances.

Other features


Enable double-checking of all terms using the internal typechecker. Off by default.


New in version 2.6.2.

Opposite of --double-check. On by default.

--guardedness, --no-guardedness

New in version 2.6.0.

Enable [disable] constructor-based guarded corecursion (see Coinduction).

The option --guardedness is inconsistent with sized types, thus, it cannot be used with both --safe and --sized-types.

Default: --no-guardedness (since 2.6.2).

--irrelevant-projections, --no-irrelevant-projections

New in version 2.5.4.

Enable [disable] projection of irrelevant record fields (see Irrelevance). The option --irrelevant-projections makes Agda inconsistent.

Default (since version 2.6.1): --no-irrelevant-projections.


New in version 2.6.2.

Turn on automatic compile-time inlining. See The INLINE and NOINLINE pragmas for more information.


New in version 2.5.4.

Disable automatic compile-time inlining (default). Only definitions marked INLINE will be inlined. On by default.


New in version 2.6.0.

Disable reduction using the Agda Abstract Machine.


New in version 2.6.2.

Disable call-by-need evaluation in the Agda Abstract Machine.


New in version 2.2.10.

Disable the forcing optimisation. Since Agda 2.6.1 it is a pragma option.


New in version 2.5.4.

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.


New in version 2.6.0.

Disable the syntactic equality shortcut in the conversion checker.


New in version 2.6.3.

Give the syntactic equality shortcut N units of fuel (N must be a natural number).

If N is omitted, then the syntactic equality shortcut is enabled without any restrictions. (This is the default.)

If N is given, then the syntactic equality shortcut is given N units of fuel. The exact meaning of this is implementation-dependent, but successful uses of the shortcut do not affect the amount of fuel.

Note that this option is experimental and subject to change.


New in version 2.3.0.

Disable postulates, unsafe OPTIONS pragmas and primTrustMe. Prevents to have both --sized-types and --guardedness on. Further reading: Safe Agda.

--sized-types, --no-sized-types

New in version 2.2.0.

Enable [disable] sized types (see Sized Types).

The option --sized-types is inconsistent with constructor-based guarded corecursion, thus, it cannot be used with both --safe and --guardedness.

Default: --no-sized-types (since 2.6.2).


Ignore universe levels (this makes Agda inconsistent; see type-in-type).


New in version 2.6.0.

Enable typing rule Setω : Setω (this makes Agda inconsistent; see omega-in-omega).

--universe-polymorphism, --no-universe-polymorphism

New in version 2.3.0.

Enable [disable] universe polymorphism (see Universe Levels).

Default: --universe-polymorphism.

--cumulativity, --no-cumulativity

New in version 2.6.1.

Enable [disable] cumulative subtyping of universes, i.e., if A : Set i then also A : Set j for all j >= i.

Default: --no-cumulativity.


New in version 2.6.2.

Disable the implicit statement open import Agda.Primitive using (Set; Prop) at the start of each top-level Agda module.


New in version 2.6.3.

Do not load the primitive modules (Agda.Primitive, Agda.Primitive.Cubical) when type-checking this program. This is useful if you want to declare Agda’s very magical primitives in a Literate Agda file of your choice.

If you are using this option, it is your responsibility to ensure that all of the BUILTIN things defined in those modules are loaded. Agda will not work otherwise.

Incompatible with --safe.

--save-metas, --no-save-metas

New in version 2.6.3.

Save [or do not save] meta-variables in .agdai files. The alternative is to expand the meta-variables to their definitions. This option can affect performance. The default is to not save the meta-variables.


New in version 2.6.3.

Automatically marks parameters to record projections and definitions in a record module as erased.


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.

The command agda --help=warning provides information about which warnings are turned on by default.

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.


Importing a file not using e.g. --safe from one which does.


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.


Importing a file using e.g. --cubical into one which doesn’t.


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.


Run Agda with all warnings enabled, except for warnings about empty abstract blocks:

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

Run Agda on a file which uses the standard library. Note that you must have already created a libraries file as described in Library Management.

agda -l standard-library -i. file.agda

(Or if you have added standard-library to your defaults file, simply agda 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:

Furthermore --cubical and --erased-cubical are jointly infective: if one of them is used in one module, then one or the other must be used in all modules that depend on this module.

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:

Furthermore the option --cubical-compatible is mostly coinfective. If a module uses --cubical-compatible then all modules that this module imports (directly) must also use --cubical-compatible, with the following exception: if a module uses both --cubical-compatible and --with-K, then it is not required to use --cubical-compatible in (directly) imported modules that use --with-K. (Note that one cannot use --cubical-compatible and --with-K at the same time if --safe is used.)

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: