<!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.Polarity</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.Polarity</p></div><div id="interface"><h1>Polarity lattice.
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:-47--92-" target="main">(/\)</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:neg" target="main">neg</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:composePol" target="main">composePol</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:polFromOcc" target="main">polFromOcc</a></p></div><h1>Auxiliary functions
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:nextPolarity" target="main">nextPolarity</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:purgeNonvariant" target="main">purgeNonvariant</a></p></div><h1>Computing the polarity of a symbol.
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:computePolarity" target="main">computePolarity</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:enablePhantomTypes" target="main">enablePhantomTypes</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:dependentPolarity" target="main">dependentPolarity</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:relevantInIgnoringNonvariant" target="main">relevantInIgnoringNonvariant</a></p></div><h1>Turn polarity <code><a href="Agda-TypeChecking-Monad-Base.html#v:Nonvariant">Nonvariant</a></code> into relevance <code><a href="Agda-Syntax-Common.html#v:UnusedArg">UnusedArg</a></code>
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:mkUnused" target="main">mkUnused</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:nonvariantToUnusedArg" target="main">nonvariantToUnusedArg</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:nonvariantToUnusedArgInDef" target="main">nonvariantToUnusedArgInDef</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:nonvariantToUnusedArgInClause" target="main">nonvariantToUnusedArgInClause</a></p></div><h1>Sized types
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:sizePolarity" target="main">sizePolarity</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:checkSizeIndex" target="main">checkSizeIndex</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a href="Agda-TypeChecking-Polarity.html#t:HasPolarity" target="main">HasPolarity</a> a</p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Polarity.html#v:polarity" target="main">polarity</a></p></div></div></body></html>
