Documentation

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 ~.agdadefaults

• optUseLibs :: Bool

  look for .agda-lib files

• optTrustedExecutables :: Map ExeName FilePath

  Map names of trusted executables to absolute paths

• optPrintAgdaDir :: Bool
   
• optPrintVersion :: Bool
   
• optPrintHelp :: Maybe Help
   
• optInteractive :: Bool

  Agda REPL (-I).

• optGHCiInteraction :: Bool
   
• optJSONInteraction :: Bool
   
• 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
   
• optLocalInterfaces :: 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?

Fields

• optShowImplicit :: Bool
   
• optShowIrrelevant :: Bool
   
• optUseUnicode :: UnicodeOrAscii
   
• optVerbose :: !Verbosity
   
• optProfiling :: ProfileOptions
   
• optProp :: Bool
   
• optTwoLevel :: WithDefault 'False
   
• optAllowUnsolved :: Bool
   
• optAllowIncompleteMatch :: Bool
   
• optDisablePositivity :: Bool
   
• optTerminationCheck :: Bool
   
• optTerminationDepth :: CutOff

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

• optUniverseCheck :: Bool
   
• optOmegaInOmega :: Bool
   
• optCumulativity :: Bool
   
• optSizedTypes :: WithDefault 'False
   
• optGuardedness :: WithDefault 'False
   
• optInjectiveTypeConstructors :: Bool
   
• optUniversePolymorphism :: Bool
   
• optIrrelevantProjections :: Bool
   
• optExperimentalIrrelevance :: Bool

  irrelevant levels, irrelevant data matching

• optWithoutK :: WithDefault 'False
   
• optCubicalCompatible :: WithDefault 'False
   
• optCopatterns :: Bool

  Allow definitions by copattern matching?

• optPatternMatching :: Bool

  Is pattern matching allowed in the current file?

• optExactSplit :: Bool
   
• optEta :: Bool
   
• optForcing :: Bool

  Perform the forcing analysis on data constructors?

• optProjectionLike :: Bool

  Perform the projection-likeness analysis on functions?

• optEraseRecordParameters :: Bool

  Mark parameters of record modules as erased?

• optRewriting :: Bool

  Can rewrite rules be added and used?

• optCubical :: Maybe Cubical
   
• optGuarded :: Bool
   
• optFirstOrder :: Bool

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

• optPostfixProjections :: Bool

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

• optKeepPatternVariables :: Bool

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

• optInstanceSearchDepth :: Int
   
• optOverlappingInstances :: Bool
   
• optQualifiedInstances :: Bool

  Should instance search consider instances with qualified names?

• optInversionMaxDepth :: Int
   
• optSafe :: Bool
   
• optDoubleCheck :: Bool
   
• 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
   
• optCompileNoMain :: Bool
   
• optCaching :: Bool
   
• optCountClusters :: Bool

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

• optAutoInline :: Bool

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

• optPrintPatternSynonyms :: Bool
   
• optFastReduce :: Bool

  Use the Agda abstract machine (fastReduce)?

• optCallByName :: Bool

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

• optConfluenceCheck :: Maybe ConfluenceCheck

  Check confluence of rewrite rules?

• optCohesion :: Bool

  Are the cohesion modalities available?

• optFlatSplit :: WithDefault 'False

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

• optImportSorts :: Bool

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

• optLoadPrimitives :: Bool

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

• optAllowExec :: Bool
   
• optSaveMetas :: WithDefault 'False

  Save meta-variables.

• optShowIdentitySubstitutions :: Bool

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

• optKeepCoveringClauses :: Bool

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

Fields

• oldOptionName :: String
   
• newOptionName :: String
   

Fields

• _warningSet :: Set WarningName
   
• _warn2Error :: Bool
   

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.