<!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.Context</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();};
//]]>
</script></head><body id="mini"><div id="module-header"><p class="caption">Agda.TypeChecking.Monad.Context</p></div><div id="interface"><h1>Modifying the context
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:modifyContextEntry" target="main">modifyContextEntry</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:modifyContextEntries" target="main">modifyContextEntries</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:modifyContext" target="main">modifyContext</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:mkContextEntry" target="main">mkContextEntry</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:inContext" target="main">inContext</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:inTopContext" target="main">inTopContext</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:escapeContext" target="main">escapeContext</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:escapeContextToTopLevel" target="main">escapeContextToTopLevel</a></p></div><h1>Adding to the context
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtx" target="main">addCtx</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:addContext" target="main">addContext</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtxs" target="main">addCtxs</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtxString" target="main">addCtxString</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtxString_" target="main">addCtxString_</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:dummyDom" target="main">dummyDom</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:underAbstraction" target="main">underAbstraction</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:underAbstraction_" target="main">underAbstraction_</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:addCtxTel" target="main">addCtxTel</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:addLetBinding" target="main">addLetBinding</a></p></div><h1>Querying the context
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:getContext" target="main">getContext</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:getContextSize" target="main">getContextSize</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:getContextArgs" target="main">getContextArgs</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:getContextTerms" target="main">getContextTerms</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:getContextTelescope" target="main">getContextTelescope</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:getContextId" target="main">getContextId</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:typeOfBV-39-" target="main">typeOfBV'</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:typeOfBV" target="main">typeOfBV</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:nameOfBV" target="main">nameOfBV</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:-33--33--33-" target="main">(!!!)</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Monad-Context.html#v:getVarInfo" target="main">getVarInfo</a></p></div></div></body></html>
