<!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.Term</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.Term</p></div><div id="interface"><h1>Types
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:isType" target="main">isType</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:isType_" target="main">isType_</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:isTypeEqualTo" target="main">isTypeEqualTo</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:leqType_" target="main">leqType_</a></p></div><h1>Telescopes
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkTelescope_" target="main">checkTelescope_</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkTypedBindings_" target="main">checkTypedBindings_</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a href="Agda-TypeChecking-Rules-Term.html#t:LamOrPi" target="main">LamOrPi</a> </p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkTypedBindings" target="main">checkTypedBindings</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkTypedBinding" target="main">checkTypedBinding</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkLambda" target="main">checkLambda</a></p></div><h1>Literal
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkLiteral" target="main">checkLiteral</a></p></div><h1>Terms
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:reduceCon" target="main">reduceCon</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkArguments-39-" target="main">checkArguments'</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:unScope" target="main">unScope</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkExpr" target="main">checkExpr</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:domainFree" target="main">domainFree</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkMeta" target="main">checkMeta</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:inferMeta" target="main">inferMeta</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:inferHead" target="main">inferHead</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:inferDef" target="main">inferDef</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkConstructorApplication" target="main">checkConstructorApplication</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkHeadApplication" target="main">checkHeadApplication</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:traceCallE" target="main">traceCallE</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkArguments" target="main">checkArguments</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkArguments_" target="main">checkArguments_</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:inferExpr" target="main">inferExpr</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:defOrVar" target="main">defOrVar</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:inferOrCheck" target="main">inferOrCheck</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:inferExprForWith" target="main">inferExprForWith</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkTerm" target="main">checkTerm</a></p></div><h1>Let bindings
</h1><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkLetBindings" target="main">checkLetBindings</a></p></div><div class="top"><p class="src"><a href="Agda-TypeChecking-Rules-Term.html#v:checkLetBinding" target="main">checkLetBinding</a></p></div></div></body></html>
