Documentation

Fields

• :: forall (a :: Bool) (b :: Bool). String
   
• -> Bool
   
• -> (PragmaOptions -> WithDefault a)
   
• -> String
   
• -> Bool
   
• -> (PragmaOptions -> WithDefault b)
   
• -> ImpliedPragmaOption

  The first option having the given value implies the second option having its given value. For instance, `ImpliesPragmaOption "lossy-unification" True _optFirstOrder "require-unique-meta-solutions" False _optRequireUniqueMetaSolutions` encodes the fact that --lossy-unification implies --no-require-unique-meta-solutions.

Fields

• icOptionActive :: PragmaOptions -> Bool

  Is the option active?

• icOptionDescription :: String

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

• icOptionKind :: InfectiveCoinfective

  Is the option (roughly speaking) infective or coinfective?

• icOptionOK :: PragmaOptions -> PragmaOptions -> Bool

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

• icOptionWarning :: TopLevelModuleName -> Doc

  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.

Fields

• oldOptionName :: String
   
• newOptionName :: String
   

Fields

• optProgramName :: String
   
• optInputFile :: Maybe FilePath
   
• optIncludePaths :: [FilePath]
   
• optAbsoluteIncludePaths :: [AbsolutePath]

  The list should not contain duplicates.

• optLibraries :: [LibName]
   
• optOverrideLibrariesFile :: Maybe FilePath

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

• optDefaultLibs :: Bool

  Use ~/.agda/defaults.

• optUseLibs :: Bool

  look for .agda-lib files.

• optTraceImports :: Integer

  Configure notifications about imported modules.

• optTrustedExecutables :: Map ExeName FilePath

  Map names of trusted executables to absolute paths.

• optPrintAgdaDataDir :: Bool
   
• optPrintAgdaAppDir :: Bool
   
• optPrintVersion :: Maybe PrintAgdaVersion
   
• optPrintHelp :: Maybe Help
   
• optBuildLibrary :: Bool

  --build-library: Build all modules in the current library.

• optSetup :: Bool

  Force Agda to self-setup at startup.

• optEmacsMode :: Set EmacsModeCommand

  Emacs mode administration (formerly done by the agda-mode executable). Accepted subcommands: locate, setup, compile. Can be given several times, subcommands are accumulated in the set.

• optInteractive :: Bool

  Agda REPL (-I).

• optGHCiInteraction :: Bool

  --interaction mode.

• optJSONInteraction :: Bool

  --interaction-json mode.

• optExitOnError :: !Bool

  Exit if an interactive command fails.

• optCompileDir :: Maybe FilePath

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

• optGenerateVimFile :: Bool
   
• optIgnoreInterfaces :: Bool
   
• optIgnoreAllInterfaces :: Bool
   
• optPragmaOptions :: PragmaOptions
   
• optOnlyScopeChecking :: Bool

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

• optTransliterate :: Bool

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

• optDiagnosticsColour :: DiagnosticsColours

  Configure colour output.

Fields

• _optShowImplicit :: WithDefault 'False
   
• _optShowGeneralized :: WithDefault 'True

  Show generalized parameters in Pi types

• _optShowIrrelevant :: WithDefault 'False
   
• _optUseUnicode :: WithDefault' UnicodeOrAscii 'True
   
• _optVerbose :: !Verbosity
   
• _optProfiling :: ProfileOptions
   
• _optProp :: WithDefault 'False
   
• _optLevelUniverse :: WithDefault 'False
   
• _optTwoLevel :: WithDefault 'False
   
• _optAllowUnsolved :: WithDefault 'False
   
• _optAllowIncompleteMatch :: WithDefault 'False
   
• _optPositivityCheck :: WithDefault 'True
   
• _optTerminationCheck :: WithDefault 'True
   
• _optTerminationDepth :: CutOff

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

• _optUniverseCheck :: WithDefault 'True
   
• _optOmegaInOmega :: WithDefault 'False
   
• _optCumulativity :: WithDefault 'False
   
• _optSizedTypes :: WithDefault 'False
   
• _optGuardedness :: WithDefault 'False
   
• _optInjectiveTypeConstructors :: WithDefault 'False
   
• _optUniversePolymorphism :: WithDefault 'True
   
• _optIrrelevantProjections :: WithDefault 'False
   
• _optExperimentalIrrelevance :: WithDefault 'False

  irrelevant levels, irrelevant data matching

• _optWithoutK :: WithDefault 'False
   
• _optCubicalCompatible :: WithDefault 'False
   
• _optCopatterns :: WithDefault 'True

  Allow definitions by copattern matching?

• _optPatternMatching :: WithDefault 'True

  Is pattern matching allowed in the current file?

• _optExactSplit :: WithDefault 'False
   
• _optHiddenArgumentPuns :: WithDefault 'False

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

• _optEta :: WithDefault 'True
   
• _optForcing :: WithDefault 'True

  Perform the forcing analysis on data constructors?

• _optProjectionLike :: WithDefault 'True

  Perform the projection-likeness analysis on functions?

• _optErasure :: WithDefault 'False
   
• _optErasedMatches :: WithDefault 'True

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

• _optEraseRecordParameters :: WithDefault 'False

  Mark parameters of record modules as erased?

• _optRewriting :: WithDefault 'False

  Can rewrite rules be added and used?

• _optCubical :: Maybe Cubical
   
• _optGuarded :: WithDefault 'False
   
• _optFirstOrder :: WithDefault 'False

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

• _optRequireUniqueMetaSolutions :: WithDefault 'True

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

• _optPostfixProjections :: WithDefault 'True

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

• _optKeepPatternVariables :: WithDefault 'True

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

• _optInferAbsurdClauses :: WithDefault '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.

• _optInstanceSearchDepth :: Int
   
• _optBacktrackingInstances :: WithDefault 'False
   
• _optQualifiedInstances :: WithDefault 'True

  Should instance search consider instances with qualified names?

• _optInversionMaxDepth :: Int
   
• _optSafe :: WithDefault 'False
   
• _optDoubleCheck :: WithDefault 'False
   
• _optSyntacticEquality :: !(Maybe Int)

  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.

• _optWarningMode :: WarningMode
   
• _optCompileMain :: WithDefault 'True

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

• _optCaching :: WithDefault 'True
   
• _optCountClusters :: WithDefault 'False

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

• _optAutoInline :: WithDefault 'False

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

• _optPrintPatternSynonyms :: WithDefault 'True
   
• _optFastReduce :: WithDefault 'True

  Use the Agda abstract machine (fastReduce)?

• _optCallByName :: WithDefault 'False

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

• _optConfluenceCheck :: Maybe ConfluenceCheck

  Check confluence of rewrite rules?

• _optCohesion :: WithDefault 'False

  Are the cohesion modalities available?

• _optFlatSplit :: WithDefault 'False

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

• _optPolarity :: WithDefault 'False

  Can we use modal polarities (++, +, etc.)?

• _optImportSorts :: WithDefault 'True

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

• _optLoadPrimitives :: WithDefault 'True

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

• _optAllowExec :: WithDefault 'False

  Allow running external executables from meta programs.

• _optSaveMetas :: WithDefault 'False

  Save meta-variables to interface files.

• _optShowIdentitySubstitutions :: WithDefault 'False

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

• _optKeepCoveringClauses :: WithDefault 'False

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

• _optLargeIndices :: WithDefault 'False

  Allow large indices, and large forced arguments in constructors.

• _optForcedArgumentRecursion :: WithDefault 'True

  Allow recursion on forced constructor arguments.