<!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.Rules.LHS.Unify</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.Rules.LHS.Unify</p></div><div id="interface"><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unify" target="main">Unify</a> a</p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyMayPostpone" target="main">UnifyMayPostpone</a> </p></div><div class="top"><p class="src"><span class="keyword">type</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyEnv" target="main">UnifyEnv</a> </p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:emptyUEnv" target="main">emptyUEnv</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:noPostponing" target="main">noPostponing</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:askPostpone" target="main">askPostpone</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyOutput" target="main">UnifyOutput</a> </p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:emptyUOutput" target="main">emptyUOutput</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Unifiable" target="main">Unifiable</a> </p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:reportPostponing" target="main">reportPostponing</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:ifClean" target="main">ifClean</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Equality" target="main">Equality</a> </p></div><div class="top"><p class="src"><span class="keyword">type</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:Sub" target="main">Sub</a> </p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyException" target="main">UnifyException</a> </p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnifyState" target="main">UnifyState</a> </p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:emptyUState" target="main">emptyUState</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:constructorMismatch" target="main">constructorMismatch</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:constructorMismatchHH" target="main">constructorMismatchHH</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:onSub" target="main">onSub</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:modSub" target="main">modSub</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:checkEqualities" target="main">checkEqualities</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:checkEquality" target="main">checkEquality</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:checkEqualityHH" target="main">checkEqualityHH</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:forceHom" target="main">forceHom</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:addEquality" target="main">addEquality</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:addEqualityHH" target="main">addEqualityHH</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:takeEqualities" target="main">takeEqualities</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:occursCheck" target="main">occursCheck</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:-124--45--62-" target="main">(|->)</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:makeSubstitution" target="main">makeSubstitution</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UReduce" target="main">UReduce</a> t</p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:flattenSubstitution" target="main">flattenSubstitution</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:UnificationResult" target="main">UnificationResult</a> </p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:HomHet" target="main">HomHet</a> a</p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:isHom" target="main">isHom</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:fromHom" target="main">fromHom</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:leftHH" target="main">leftHH</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:rightHH" target="main">rightHH</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TermHH" target="main">TermHH</a> </p></div><div class="top"><p class="src"><span class="keyword">type</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TypeHH" target="main">TypeHH</a> </p></div><div class="top"><p class="src"><span class="keyword">type</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TelHH" target="main">TelHH</a> </p></div><div class="top"><p class="src"><span class="keyword">type</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:TelViewHH" target="main">TelViewHH</a> </p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:absAppHH" target="main">absAppHH</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ApplyHH" target="main">ApplyHH</a> t</p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:substHH" target="main">substHH</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:SubstHH" target="main">SubstHH</a> t tHH</p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:unifyIndices_" target="main">unifyIndices_</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:unifyIndices" target="main">unifyIndices</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:dataOrRecordType" target="main">dataOrRecordType</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:dataOrRecordType-39-" target="main">dataOrRecordType'</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:dataOrRecordTypeHH" target="main">dataOrRecordTypeHH</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:isEtaRecordTypeHH" target="main">isEtaRecordTypeHH</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-LHS-Unify.html#t:ShapeView" target="main">ShapeView</a> a</p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:shapeView" target="main">shapeView</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:shapeViewHH" target="main">shapeViewHH</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-LHS-Unify.html#v:telViewUpToHH" target="main">telViewUpToHH</a></p></div></div></body></html>
