Agda.Interaction.Options

The list should not contain duplicates.

Use this (if Just) instead of ~/.agda/libraries.

Use ~/.agda/defaults.

look for .agda-lib files.

Configure notifications about imported modules.

Map names of trusted executables to absolute paths.

Agda REPL (-I).

Exit if an interactive command fails.

In the absence of a path the project root is used.

Should the top-level module only be scope-checked, and not type-checked?

Should code points that are not supported by the locale be transliterated?

Configure colour output.

Show generalized parameters in Pi types

Cut off structural order comparison at some depth in termination checker?

irrelevant levels, irrelevant data matching

Allow definitions by copattern matching?

Is pattern matching allowed in the current file?

Should patterns of the form {x} or ⦃ x ⦄ be interpreted as puns?

Perform the forcing analysis on data constructors?

Perform the projection-likeness analysis on functions?

Allow matching in erased positions for single-constructor, non-indexed data/record types. (This kind of matching is always allowed for record types with η-equality.)

Mark parameters of record modules as erased?

Can rewrite rules be added and used?

Should we speculatively unify function applications as if they were injective? Implies optRequireUniqueMetaSolutions.

Forbid non-unique meta solutions allowed. For instance from INJECTIVE_FOR_INFERENCE pragmas.

Should system generated projections ProjSystem be printed postfix (True) or prefix (False).

Should case splitting replace variables with dot patterns (False) or keep them as variables (True).

Should case splitting and coverage checking try to discharge absurd clauses? Default: True, but False might make coverage checking considerably faster in some cases.

Should instance search consider instances with qualified names?

Should the conversion checker use the syntactic equality shortcut? Nothing means that it should. Just n, for a non-negative number n, means that syntactic equality checking gets n units of fuel. If the fuel becomes zero, then syntactic equality checking is turned off. The fuel counter is decreased in the failure continuation of checkSyntacticEquality.

Treat the module given at the command line or via interaction as main module in compilation?

Count extended grapheme clusters rather than code points when generating LaTeX.

Automatic compile-time inlining for simple definitions (unless marked NOINLINE).

Use the Agda abstract machine (fastReduce)?

Use call-by-name instead of call-by-need.

Check confluence of rewrite rules?

Are the cohesion modalities available?

Can we split on a (@flat x : A) argument?

Should every top-level module start with an implicit statement open import Agda.Primitive using (Set; Prop)?

Should we load the primitive modules at all? This is a stronger form of optImportSorts.

Allow running external executables from meta programs.

Save meta-variables to interface files.

Show identity substitutions when pretty-printing terms (i.e. always show all arguments of a metavariable).

Do not discard clauses constructed by the coverage checker (needed for some external backends).

Allow large indices, and large forced arguments in constructors.

Allow recursion on forced constructor arguments.

Is the option active?

A description of the option (typically a flag that activates the option).

Is the option (roughly speaking) infective or coinfective?

This function returns True exactly when, from the perspective of the option in question, the options in the current module (the first argument) are compatible with the options in a given imported module (the second argument).

A warning message that should be used if this option is not used correctly. The given module name is the name of an imported module for which icOptionOK failed.