<!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.TypeChecking.Monad.Signature</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-TypeChecking-Monad-Signature.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-Monad-Signature.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.TypeChecking.Monad.Signature</p></div><div id="table-of-contents"><p class="caption">Contents</p><ul><li><a href="#g:1">modifiers for parts of the signature
</a></li></ul></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"><a href="#v:modifySignature">modifySignature</a> :: (<a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:modifyImportedSignature">modifyImportedSignature</a> :: (<a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:getSignature">getSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a></li><li class="src short"><a href="#v:getImportedSignature">getImportedSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a></li><li class="src short"><a href="#v:setSignature">setSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:setImportedSignature">setImportedSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:withSignature">withSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li><li class="src short"><a href="#v:updateDefinition">updateDefinition</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> (<a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a></li><li class="src short"><a href="#v:updateTheDef">updateTheDef</a> :: (<a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></li><li class="src short"><a href="#v:updateDefType">updateDefType</a> :: (<a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></li><li class="src short"><a href="#v:updateDefArgOccurrences">updateDefArgOccurrences</a> :: ([<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>] -> [<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>]) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></li><li class="src short"><a href="#v:updateDefPolarity">updateDefPolarity</a> :: ([<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>] -> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>]) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></li><li class="src short"><a href="#v:updateDefCompiledRep">updateDefCompiledRep</a> :: (<a href="Agda-TypeChecking-Monad-Base.html#t:CompiledRepresentation">CompiledRepresentation</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:CompiledRepresentation">CompiledRepresentation</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></li><li class="src short"><a href="#v:addConstant">addConstant</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:setTerminates">setTerminates</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:addHaskellCode">addHaskellCode</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellType">HaskellType</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellCode">HaskellCode</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:addHaskellType">addHaskellType</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellType">HaskellType</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:addEpicCode">addEpicCode</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:EpicCode">EpicCode</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:addJSCode">addJSCode</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:markStatic">markStatic</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:unionSignatures">unionSignatures</a> :: [<a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a></li><li class="src short"><a href="#v:addSection">addSection</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:lookupSection">lookupSection</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a></li><li class="src short"><a href="#v:addDisplayForms">addDisplayForms</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:applySection">applySection</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:addDisplayForm">addDisplayForm</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayForm">DisplayForm</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:canonicalName">canonicalName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a></li><li class="src short"><a href="#v:whatInduction">whatInduction</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a></li><li class="src short"><a href="#v:singleConstructorType">singleConstructorType</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:getConstInfo">getConstInfo</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> tcm => <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> tcm <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></li><li class="src short"><a href="#v:getPolarity">getPolarity</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>]</li><li class="src short"><a href="#v:getPolarity-39-">getPolarity'</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>]</li><li class="src short"><a href="#v:setPolarity">setPolarity</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:getArgOccurrences">getArgOccurrences</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>]</li><li class="src short"><a href="#v:getArgOccurrence">getArgOccurrence</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a></li><li class="src short"><a href="#v:setArgOccurrences">setArgOccurrences</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:getMutual">getMutual</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>]</li><li class="src short"><a href="#v:setMutual">setMutual</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:mutuallyRecursive">mutuallyRecursive</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:getSecFreeVars">getSecFreeVars</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></li><li class="src short"><a href="#v:getModuleFreeVars">getModuleFreeVars</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></li><li class="src short"><a href="#v:getDefFreeVars">getDefFreeVars</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></li><li class="src short"><a href="#v:freeVarsToApply">freeVarsToApply</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Args">Args</a></li><li class="src short"><a href="#v:instantiateDef">instantiateDef</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></li><li class="src short"><a href="#v:makeAbstract">makeAbstract</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a></li><li class="src short"><a href="#v:inAbstractMode">inAbstractMode</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li><li class="src short"><a href="#v:inConcreteMode">inConcreteMode</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li><li class="src short"><a href="#v:ignoreAbstractMode">ignoreAbstractMode</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a</li><li class="src short"><a href="#v:treatAbstractly">treatAbstractly</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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:treatAbstractly-39-">treatAbstractly'</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCEnv">TCEnv</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:typeOfConst">typeOfConst</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></li><li class="src short"><a href="#v:relOfConst">relOfConst</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a></li><li class="src short"><a href="#v:sortOfConst">sortOfConst</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></li><li class="src short"><a href="#v:isProjection">isProjection</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>))</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:modifySignature" class="def">modifySignature</a> :: (<a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#modifySignature" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:modifyImportedSignature" class="def">modifyImportedSignature</a> :: (<a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#modifyImportedSignature" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getSignature" class="def">getSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a><a href="src/Agda-TypeChecking-Monad-Signature.html#getSignature" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getImportedSignature" class="def">getImportedSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a><a href="src/Agda-TypeChecking-Monad-Signature.html#getImportedSignature" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:setSignature" class="def">setSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#setSignature" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:setImportedSignature" class="def">setImportedSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#setImportedSignature" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:withSignature" class="def">withSignature</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-TypeChecking-Monad-Signature.html#withSignature" class="link">Source</a></p></div><h1 id="g:1">modifiers for parts of the signature
</h1><div class="top"><p class="src"><a name="v:updateDefinition" class="def">updateDefinition</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> (<a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a><a href="src/Agda-TypeChecking-Monad-Signature.html#updateDefinition" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:updateTheDef" class="def">updateTheDef</a> :: (<a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Defn">Defn</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a><a href="src/Agda-TypeChecking-Monad-Signature.html#updateTheDef" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:updateDefType" class="def">updateDefType</a> :: (<a href="Agda-Syntax-Internal.html#t:Type">Type</a> -> <a href="Agda-Syntax-Internal.html#t:Type">Type</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a><a href="src/Agda-TypeChecking-Monad-Signature.html#updateDefType" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:updateDefArgOccurrences" class="def">updateDefArgOccurrences</a> :: ([<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>] -> [<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>]) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a><a href="src/Agda-TypeChecking-Monad-Signature.html#updateDefArgOccurrences" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:updateDefPolarity" class="def">updateDefPolarity</a> :: ([<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>] -> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>]) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a><a href="src/Agda-TypeChecking-Monad-Signature.html#updateDefPolarity" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:updateDefCompiledRep" class="def">updateDefCompiledRep</a> :: (<a href="Agda-TypeChecking-Monad-Base.html#t:CompiledRepresentation">CompiledRepresentation</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:CompiledRepresentation">CompiledRepresentation</a>) -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a><a href="src/Agda-TypeChecking-Monad-Signature.html#updateDefCompiledRep" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addConstant" class="def">addConstant</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#addConstant" class="link">Source</a></p><div class="doc"><p>Add a constant to the signature. Lifts the definition to top level.
</p></div></div><div class="top"><p class="src"><a name="v:setTerminates" class="def">setTerminates</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#setTerminates" class="link">Source</a></p><div class="doc"><p>Set termination info of a defined function symbol.
</p></div></div><div class="top"><p class="src"><a name="v:addHaskellCode" class="def">addHaskellCode</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellType">HaskellType</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellCode">HaskellCode</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#addHaskellCode" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addHaskellType" class="def">addHaskellType</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:HaskellType">HaskellType</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#addHaskellType" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addEpicCode" class="def">addEpicCode</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:EpicCode">EpicCode</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#addEpicCode" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addJSCode" class="def">addJSCode</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#addJSCode" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:markStatic" class="def">markStatic</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#markStatic" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:unionSignatures" class="def">unionSignatures</a> :: [<a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:Signature">Signature</a><a href="src/Agda-TypeChecking-Monad-Signature.html#unionSignatures" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addSection" class="def">addSection</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#addSection" class="link">Source</a></p><div class="doc"><p>Add a section to the signature.
</p></div></div><div class="top"><p class="src"><a name="v:lookupSection" class="def">lookupSection</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a><a href="src/Agda-TypeChecking-Monad-Signature.html#lookupSection" class="link">Source</a></p><div class="doc"><p>Lookup a section. If it doesn't exist that just means that the module
wasn't parameterised.
</p></div></div><div class="top"><p class="src"><a name="v:addDisplayForms" class="def">addDisplayForms</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#addDisplayForms" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:applySection" class="def">applySection</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Internal.html#t:Telescope">Telescope</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-Syntax-Internal.html#t:Args">Args</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="/usr/share/doc/ghc/html/libraries/containers-0.4.2.1/Data-Map.html#t:Map">Map</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#applySection" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addDisplayForm" class="def">addDisplayForm</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:DisplayForm">DisplayForm</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#addDisplayForm" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:canonicalName" class="def">canonicalName</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a><a href="src/Agda-TypeChecking-Monad-Signature.html#canonicalName" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:whatInduction" class="def">whatInduction</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Induction">Induction</a><a href="src/Agda-TypeChecking-Monad-Signature.html#whatInduction" class="link">Source</a></p><div class="doc"><p>Can be called on either a (co)datatype, a record type or a
(co)constructor.
</p></div></div><div class="top"><p class="src"><a name="v:singleConstructorType" class="def">singleConstructorType</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#singleConstructorType" class="link">Source</a></p><div class="doc"><p>Does the given constructor come from a single-constructor type?
</p><p>Precondition: The name has to refer to a constructor.
</p></div></div><div class="top"><p class="src"><a name="v:getConstInfo" class="def">getConstInfo</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:MonadTCM">MonadTCM</a> tcm => <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> tcm <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a><a href="src/Agda-TypeChecking-Monad-Signature.html#getConstInfo" class="link">Source</a></p><div class="doc"><p>Lookup the definition of a name. The result is a closed thing, all free
variables have been abstracted over.
</p></div></div><div class="top"><p class="src"><a name="v:getPolarity" class="def">getPolarity</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>]<a href="src/Agda-TypeChecking-Monad-Signature.html#getPolarity" class="link">Source</a></p><div class="doc"><p>Look up the polarity of a definition.
</p></div></div><div class="top"><p class="src"><a name="v:getPolarity-39-" class="def">getPolarity'</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>]<a href="src/Agda-TypeChecking-Monad-Signature.html#getPolarity%27" class="link">Source</a></p><div class="doc"><p>Look up polarity of a definition and compose with polarity
represented by <code><a href="Agda-TypeChecking-Monad-Base.html#t:Comparison">Comparison</a></code>.
</p></div></div><div class="top"><p class="src"><a name="v:setPolarity" class="def">setPolarity</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-TypeChecking-Monad-Base.html#t:Polarity">Polarity</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#setPolarity" class="link">Source</a></p><div class="doc"><p>Set the polarity of a definition.
</p></div></div><div class="top"><p class="src"><a name="v:getArgOccurrences" class="def">getArgOccurrences</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>]<a href="src/Agda-TypeChecking-Monad-Signature.html#getArgOccurrences" class="link">Source</a></p><div class="doc"><p>Return a finite list of argument occurrences.
</p></div></div><div class="top"><p class="src"><a name="v:getArgOccurrence" class="def">getArgOccurrence</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a><a href="src/Agda-TypeChecking-Monad-Signature.html#getArgOccurrence" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:setArgOccurrences" class="def">setArgOccurrences</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-TypeChecking-Monad-Base.html#t:Occurrence">Occurrence</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#setArgOccurrences" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getMutual" class="def">getMutual</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> [<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>]<a href="src/Agda-TypeChecking-Monad-Signature.html#getMutual" class="link">Source</a></p><div class="doc"><p>Get the mutually recursive identifiers.
</p></div></div><div class="top"><p class="src"><a name="v:setMutual" class="def">setMutual</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> [<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>] -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#setMutual" class="link">Source</a></p><div class="doc"><p>Set the mutually recursive identifiers.
</p></div></div><div class="top"><p class="src"><a name="v:mutuallyRecursive" class="def">mutuallyRecursive</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#mutuallyRecursive" class="link">Source</a></p><div class="doc"><p>Check whether two definitions are mutually recursive.
</p></div></div><div class="top"><p class="src"><a name="v:getSecFreeVars" class="def">getSecFreeVars</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a><a href="src/Agda-TypeChecking-Monad-Signature.html#getSecFreeVars" class="link">Source</a></p><div class="doc"><p>Look up the number of free variables of a section. This is equal to the
number of parameters if we're currently inside the section and 0 otherwise.
</p></div></div><div class="top"><p class="src"><a name="v:getModuleFreeVars" class="def">getModuleFreeVars</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:ModuleName">ModuleName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a><a href="src/Agda-TypeChecking-Monad-Signature.html#getModuleFreeVars" class="link">Source</a></p><div class="doc"><p>Compute the number of free variables of a module. This is the sum of
the free variables of its sections.
</p></div></div><div class="top"><p class="src"><a name="v:getDefFreeVars" class="def">getDefFreeVars</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a><a href="src/Agda-TypeChecking-Monad-Signature.html#getDefFreeVars" class="link">Source</a></p><div class="doc"><p>Compute the number of free variables of a defined name. This is the sum of
the free variables of the sections it's contained in.
</p></div></div><div class="top"><p class="src"><a name="v:freeVarsToApply" class="def">freeVarsToApply</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Args">Args</a><a href="src/Agda-TypeChecking-Monad-Signature.html#freeVarsToApply" class="link">Source</a></p><div class="doc"><p>Compute the context variables to apply a definition to.
</p></div></div><div class="top"><p class="src"><a name="v:instantiateDef" class="def">instantiateDef</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a><a href="src/Agda-TypeChecking-Monad-Signature.html#instantiateDef" class="link">Source</a></p><div class="doc"><p>Instantiate a closed definition with the correct part of the current
context.
</p></div></div><div class="top"><p class="src"><a name="v:makeAbstract" class="def">makeAbstract</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> <a href="Agda-TypeChecking-Monad-Base.html#t:Definition">Definition</a><a href="src/Agda-TypeChecking-Monad-Signature.html#makeAbstract" class="link">Source</a></p><div class="doc"><p>Give the abstract view of a definition.
</p></div></div><div class="top"><p class="src"><a name="v:inAbstractMode" class="def">inAbstractMode</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-TypeChecking-Monad-Signature.html#inAbstractMode" class="link">Source</a></p><div class="doc"><p>Enter abstract mode. Abstract definition in the current module are transparent.
</p></div></div><div class="top"><p class="src"><a name="v:inConcreteMode" class="def">inConcreteMode</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-TypeChecking-Monad-Signature.html#inConcreteMode" class="link">Source</a></p><div class="doc"><p>Not in abstract mode. All abstract definitions are opaque.
</p></div></div><div class="top"><p class="src"><a name="v:ignoreAbstractMode" class="def">ignoreAbstractMode</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> a<a href="src/Agda-TypeChecking-Monad-Signature.html#ignoreAbstractMode" class="link">Source</a></p><div class="doc"><p>Ignore abstract mode. All abstract definitions are transparent.
</p></div></div><div class="top"><p class="src"><a name="v:treatAbstractly" class="def">treatAbstractly</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</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-TypeChecking-Monad-Signature.html#treatAbstractly" class="link">Source</a></p><div class="doc"><p>Check whether a name might have to be treated abstractly (either if we're
<code><a href="Agda-TypeChecking-Monad-Signature.html#v:inAbstractMode">inAbstractMode</a></code> or it's not a local name). Returns true for things not
declared abstract as well, but for those <code><a href="Agda-TypeChecking-Monad-Signature.html#v:makeAbstract">makeAbstract</a></code> will have no effect.
</p></div></div><div class="top"><p class="src"><a name="v:treatAbstractly-39-" class="def">treatAbstractly'</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCEnv">TCEnv</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-TypeChecking-Monad-Signature.html#treatAbstractly%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:typeOfConst" class="def">typeOfConst</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a><a href="src/Agda-TypeChecking-Monad-Signature.html#typeOfConst" class="link">Source</a></p><div class="doc"><p>get type of a constant
</p></div></div><div class="top"><p class="src"><a name="v:relOfConst" class="def">relOfConst</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Relevance">Relevance</a><a href="src/Agda-TypeChecking-Monad-Signature.html#relOfConst" class="link">Source</a></p><div class="doc"><p>get relevance of a constant
</p></div></div><div class="top"><p class="src"><a name="v:sortOfConst" class="def">sortOfConst</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a><a href="src/Agda-TypeChecking-Monad-Signature.html#sortOfConst" class="link">Source</a></p><div class="doc"><p>The name must be a datatype.
</p></div></div><div class="top"><p class="src"><a name="v:isProjection" class="def">isProjection</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</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-TypeChecking-Monad-Signature.html#isProjection" class="link">Source</a></p><div class="doc"><p>Is it the name of a record projection?
</p></div></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>
