<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.Interaction.Options</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-Interaction-Options.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Interaction-Options.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.Interaction.Options</p></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:CommandLineOptions">CommandLineOptions</a> = <a href="#v:Options">Options</a> {<ul class="subs"><li><a href="#v:optProgramName">optProgramName</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></li><li><a href="#v:optInputFile">optInputFile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></li><li><a href="#v:optIncludeDirs">optIncludeDirs</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a>] [<a href="Agda-Utils-FileName.html#t:AbsolutePath">AbsolutePath</a>]</li><li><a href="#v:optShowVersion">optShowVersion</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optShowHelp">optShowHelp</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optInteractive">optInteractive</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optRunTests">optRunTests</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optGHCiInteraction">optGHCiInteraction</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optCompile">optCompile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optEpicCompile">optEpicCompile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optJSCompile">optJSCompile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optCompileDir">optCompileDir</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></li><li><a href="#v:optGenerateVimFile">optGenerateVimFile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optGenerateLaTeX">optGenerateLaTeX</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optGenerateHTML">optGenerateHTML</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optDependencyGraph">optDependencyGraph</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></li><li><a href="#v:optLaTeXDir">optLaTeXDir</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></li><li><a href="#v:optHTMLDir">optHTMLDir</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></li><li><a href="#v:optCSSFile">optCSSFile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></li><li><a href="#v:optIgnoreInterfaces">optIgnoreInterfaces</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optForcing">optForcing</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optGhcFlags">optGhcFlags</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</li><li><a href="#v:optPragmaOptions">optPragmaOptions</a> :: <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a></li><li><a href="#v:optEpicFlags">optEpicFlags</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</li><li><a href="#v:optSafe">optSafe</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li></ul>}</li><li class="src short"><span class="keyword">data</span> <a href="#t:PragmaOptions">PragmaOptions</a> = <a href="#v:PragmaOptions">PragmaOptions</a> {<ul class="subs"><li><a href="#v:optShowImplicit">optShowImplicit</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optShowIrrelevant">optShowIrrelevant</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optVerbose">optVerbose</a> :: <a href="Agda-Interaction-Options.html#t:Verbosity">Verbosity</a></li><li><a href="#v:optProofIrrelevance">optProofIrrelevance</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optAllowUnsolved">optAllowUnsolved</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optDisablePositivity">optDisablePositivity</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optTerminationCheck">optTerminationCheck</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optTerminationDepth">optTerminationDepth</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></li><li><a href="#v:optCompletenessCheck">optCompletenessCheck</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optUniverseCheck">optUniverseCheck</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optSizedTypes">optSizedTypes</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optInjectiveTypeConstructors">optInjectiveTypeConstructors</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optGuardingTypeConstructors">optGuardingTypeConstructors</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optUniversePolymorphism">optUniversePolymorphism</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optIrrelevantProjections">optIrrelevantProjections</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optExperimentalIrrelevance">optExperimentalIrrelevance</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optWithoutK">optWithoutK</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li><a href="#v:optCopatterns">optCopatterns</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li></ul>}</li><li class="src short"><span class="keyword">type</span> <a href="#t:OptionsPragma">OptionsPragma</a> = [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</li><li class="src short"><span class="keyword">type</span> <a href="#t:Flag">Flag</a> opts = opts -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> opts</li><li class="src short"><span class="keyword">type</span> <a href="#t:Verbosity">Verbosity</a> = <a href="Agda-Utils-Trie.html#t:Trie">Trie</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></li><li class="src short"><a href="#v:checkOpts">checkOpts</a> :: <a href="Agda-Interaction-Options.html#t:Flag">Flag</a> <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a></li><li class="src short"><a href="#v:parseStandardOptions">parseStandardOptions</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a></li><li class="src short"><a href="#v:parsePragmaOptions">parsePragmaOptions</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] -> <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a></li><li class="src short"><a href="#v:parsePluginOptions">parsePluginOptions</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> (<a href="Agda-Interaction-Options.html#t:Flag">Flag</a> opts)] -> <a href="Agda-Interaction-Options.html#t:Flag">Flag</a> opts</li><li class="src short"><a href="#v:defaultOptions">defaultOptions</a> :: <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a></li><li class="src short"><a href="#v:defaultInteractionOptions">defaultInteractionOptions</a> :: <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a></li><li class="src short"><a href="#v:defaultVerbosity">defaultVerbosity</a> :: <a href="Agda-Interaction-Options.html#t:Verbosity">Verbosity</a></li><li class="src short"><a href="#v:standardOptions_">standardOptions_</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a>]</li><li class="src short"><a href="#v:unsafePragmaOptions">unsafePragmaOptions</a> :: <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a> -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</li><li class="src short"><a href="#v:isLiterate">isLiterate</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:mapFlag">mapFlag</a> :: (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>) -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> a</li><li class="src short"><a href="#v:usage">usage</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a>] -> [(<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>, [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>], [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a>])] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></li><li class="src short"><a href="#v:tests">tests</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:CommandLineOptions" class="def">CommandLineOptions</a> <a href="src/Agda-Interaction-Options.html#CommandLineOptions" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Options" class="def">Options</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:optProgramName" class="def">optProgramName</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optInputFile" class="def">optInputFile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optIncludeDirs" class="def">optIncludeDirs</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a>] [<a href="Agda-Utils-FileName.html#t:AbsolutePath">AbsolutePath</a>]</dt><dd class="doc"><p><code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#v:Left">Left</a></code> is used temporarily, before the paths have
been made absolute. An empty <code><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#v:Left">Left</a></code> list is
interpreted as <code>[<a href="-.html">.</a>]</code> (see
<code><a href="Agda-TypeChecking-Monad-Options.html#v:makeIncludeDirsAbsolute">makeIncludeDirsAbsolute</a></code>).
</p></dd><dt class="src"><a name="v:optShowVersion" class="def">optShowVersion</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optShowHelp" class="def">optShowHelp</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optInteractive" class="def">optInteractive</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optRunTests" class="def">optRunTests</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optGHCiInteraction" class="def">optGHCiInteraction</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optCompile" class="def">optCompile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optEpicCompile" class="def">optEpicCompile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optJSCompile" class="def">optJSCompile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optCompileDir" class="def">optCompileDir</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></dt><dd class="doc"><p>In the absence of a path the project root is used.
</p></dd><dt class="src"><a name="v:optGenerateVimFile" class="def">optGenerateVimFile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optGenerateLaTeX" class="def">optGenerateLaTeX</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optGenerateHTML" class="def">optGenerateHTML</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optDependencyGraph" class="def">optDependencyGraph</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optLaTeXDir" class="def">optLaTeXDir</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optHTMLDir" class="def">optHTMLDir</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optCSSFile" class="def">optCSSFile</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optIgnoreInterfaces" class="def">optIgnoreInterfaces</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optForcing" class="def">optForcing</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optGhcFlags" class="def">optGhcFlags</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optPragmaOptions" class="def">optPragmaOptions</a> :: <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optEpicFlags" class="def">optEpicFlags</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optSafe" class="def">optSafe</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:CommandLineOptions" class="caption collapser" onclick="toggleSection('i:CommandLineOptions')">Instances</p><div id="section.i:CommandLineOptions" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:PragmaOptions" class="def">PragmaOptions</a> <a href="src/Agda-Interaction-Options.html#PragmaOptions" class="link">Source</a></p><div class="doc"><p>Options which can be set in a pragma.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:PragmaOptions" class="def">PragmaOptions</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:optShowImplicit" class="def">optShowImplicit</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optShowIrrelevant" class="def">optShowIrrelevant</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optVerbose" class="def">optVerbose</a> :: <a href="Agda-Interaction-Options.html#t:Verbosity">Verbosity</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optProofIrrelevance" class="def">optProofIrrelevance</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optAllowUnsolved" class="def">optAllowUnsolved</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optDisablePositivity" class="def">optDisablePositivity</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optTerminationCheck" class="def">optTerminationCheck</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optTerminationDepth" class="def">optTerminationDepth</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optCompletenessCheck" class="def">optCompletenessCheck</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optUniverseCheck" class="def">optUniverseCheck</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optSizedTypes" class="def">optSizedTypes</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optInjectiveTypeConstructors" class="def">optInjectiveTypeConstructors</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optGuardingTypeConstructors" class="def">optGuardingTypeConstructors</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optUniversePolymorphism" class="def">optUniversePolymorphism</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optIrrelevantProjections" class="def">optIrrelevantProjections</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optExperimentalIrrelevance" class="def">optExperimentalIrrelevance</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc"><p>irrelevant levels, irrelevant data matching
</p></dd><dt class="src"><a name="v:optWithoutK" class="def">optWithoutK</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:optCopatterns" class="def">optCopatterns</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc"><p>definitions by copattern matching
</p></dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:PragmaOptions" class="caption collapser" onclick="toggleSection('i:PragmaOptions')">Instances</p><div id="section.i:PragmaOptions" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:OptionsPragma" class="def">OptionsPragma</a> = [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]<a href="src/Agda-Interaction-Options.html#OptionsPragma" class="link">Source</a></p><div class="doc"><p>The options from an <code>OPTIONS</code> pragma.
</p><p>In the future it might be nice to switch to a more structured
representation. Note that, currently, there is not a one-to-one
correspondence between list elements and options.
</p></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Flag" class="def">Flag</a> opts = opts -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> opts<a href="src/Agda-Interaction-Options.html#Flag" class="link">Source</a></p><div class="doc"><p><code>f :: Flag opts</code> is an action on the option record that results from
parsing an option. <code>f opts</code> produces either an error message or an
updated options record
</p></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Verbosity" class="def">Verbosity</a> = <a href="Agda-Utils-Trie.html#t:Trie">Trie</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a><a href="src/Agda-Interaction-Options.html#Verbosity" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:checkOpts" class="def">checkOpts</a> :: <a href="Agda-Interaction-Options.html#t:Flag">Flag</a> <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a><a href="src/Agda-Interaction-Options.html#checkOpts" class="link">Source</a></p><div class="doc"><p>Checks that the given options are consistent.
</p></div></div><div class="top"><p class="src"><a name="v:parseStandardOptions" class="def">parseStandardOptions</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a><a href="src/Agda-Interaction-Options.html#parseStandardOptions" class="link">Source</a></p><div class="doc"><p>Parse the standard options.
</p></div></div><div class="top"><p class="src"><a name="v:parsePragmaOptions" class="def">parsePragmaOptions</a><a href="src/Agda-Interaction-Options.html#parsePragmaOptions" class="link">Source</a></p><div class="subs arguments"><p class="caption">Arguments</p><table><tr><td class="src">:: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]</td><td class="doc"><p>Pragma options.
</p></td></tr><tr><td class="src">-> <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a></td><td class="doc"><p>Command-line options which should be updated.
</p></td></tr><tr><td class="src">-> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a></td><td class="doc empty"> </td></tr></table></div><div class="doc"><p>Parse options from an options pragma.
</p></div></div><div class="top"><p class="src"><a name="v:parsePluginOptions" class="def">parsePluginOptions</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>] -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> (<a href="Agda-Interaction-Options.html#t:Flag">Flag</a> opts)] -> <a href="Agda-Interaction-Options.html#t:Flag">Flag</a> opts<a href="src/Agda-Interaction-Options.html#parsePluginOptions" class="link">Source</a></p><div class="doc"><p>Parse options for a plugin.
</p></div></div><div class="top"><p class="src"><a name="v:defaultOptions" class="def">defaultOptions</a> :: <a href="Agda-Interaction-Options.html#t:CommandLineOptions">CommandLineOptions</a><a href="src/Agda-Interaction-Options.html#defaultOptions" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:defaultInteractionOptions" class="def">defaultInteractionOptions</a> :: <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a><a href="src/Agda-Interaction-Options.html#defaultInteractionOptions" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:defaultVerbosity" class="def">defaultVerbosity</a> :: <a href="Agda-Interaction-Options.html#t:Verbosity">Verbosity</a><a href="src/Agda-Interaction-Options.html#defaultVerbosity" class="link">Source</a></p><div class="doc"><p>For batch usage.
</p></div></div><div class="top"><p class="src"><a name="v:standardOptions_" class="def">standardOptions_</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a>]<a href="src/Agda-Interaction-Options.html#standardOptions_" class="link">Source</a></p><div class="doc"><p>Used for printing usage info.
</p></div></div><div class="top"><p class="src"><a name="v:unsafePragmaOptions" class="def">unsafePragmaOptions</a> :: <a href="Agda-Interaction-Options.html#t:PragmaOptions">PragmaOptions</a> -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>]<a href="src/Agda-Interaction-Options.html#unsafePragmaOptions" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isLiterate" class="def">isLiterate</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:FilePath">FilePath</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Interaction-Options.html#isLiterate" class="link">Source</a></p><div class="doc"><p>This should probably go somewhere else.
</p></div></div><div class="top"><p class="src"><a name="v:mapFlag" class="def">mapFlag</a> :: (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>) -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> a<a href="src/Agda-Interaction-Options.html#mapFlag" class="link">Source</a></p><div class="doc"><p>Map a function over the long options. Also removes the short options.
Will be used to add the plugin name to the plugin options.
</p></div></div><div class="top"><p class="src"><a name="v:usage" class="def">usage</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a>] -> [(<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>, [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a>], [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-Console-GetOpt.html#t:OptDescr">OptDescr</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a>])] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a><a href="src/Agda-Interaction-Options.html#usage" class="link">Source</a></p><div class="doc"><p>The usage info message. The argument is the program name (probably
agda).
</p></div></div><div class="top"><p class="src"><a name="v:tests" class="def">tests</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Interaction-Options.html#tests" class="link">Source</a></p></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
