<!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.Auto.Typecheck</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-Auto-Typecheck.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Auto-Typecheck.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>Safe-Infered</td></tr></table><p class="caption">Agda.Auto.Typecheck</p></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:tcExp" class="def">tcExp</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-Auto-Syntax.html#t:Ctx">Ctx</a> o -> <a href="Agda-Auto-Syntax.html#t:CExp">CExp</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#tcExp" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getDatatype" class="def">getDatatype</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o, [<a href="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</a> o])) o)<a href="src/Agda-Auto-Typecheck.html#getDatatype" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:constructorImpossible" class="def">constructorImpossible</a> :: <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#constructorImpossible" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:unequals" class="def">unequals</a> :: <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> ([(<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, <a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o)] -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)) -> [(<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, <a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o)] -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#unequals" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:unequal" class="def">unequal</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> ([(<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, <a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o)] -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)) -> [(<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, <a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o)] -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#unequal" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:traversePi" class="def">traversePi</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o) o)<a href="src/Agda-Auto-Typecheck.html#traversePi" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:tcargs" class="def">tcargs</a> :: <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-Auto-Syntax.html#t:Ctx">Ctx</a> o -> <a href="Agda-Auto-Syntax.html#t:CExp">CExp</a> o -> <a href="Agda-Auto-Syntax.html#t:MArgList">MArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> (<a href="Agda-Auto-Syntax.html#t:CExp">CExp</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)) -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#tcargs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addend" class="def">addend</a> :: <a href="Agda-Auto-Syntax.html#t:FMode">FMode</a> -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> (<a href="Agda-Auto-Syntax.html#t:Exp">Exp</a> o) t -> <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> (<a href="Agda-Auto-Syntax.html#t:Exp">Exp</a> o) blk<a href="src/Agda-Auto-Typecheck.html#addend" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:copyarg" class="def">copyarg</a> :: t -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-Auto-Typecheck.html#copyarg" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:HNNBlks" class="def">HNNBlks</a> o = [<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o]<a href="src/Agda-Auto-Typecheck.html#HNNBlks" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:noblks" class="def">noblks</a> :: [a]<a href="src/Agda-Auto-Typecheck.html#noblks" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addblk" class="def">addblk</a> :: a -> [a] -> [a]<a href="src/Agda-Auto-Typecheck.html#addblk" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hnn" class="def">hnn</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o) o)<a href="src/Agda-Auto-Typecheck.html#hnn" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hnn_blks" class="def">hnn_blks</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o, <a href="Agda-Auto-Typecheck.html#t:HNNBlks">HNNBlks</a> o) o)<a href="src/Agda-Auto-Typecheck.html#hnn_blks" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hnn_checkstep" class="def">hnn_checkstep</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>) o)<a href="src/Agda-Auto-Typecheck.html#hnn_checkstep" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hnn-39-" class="def">hnn'</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o, <a href="Agda-Auto-Typecheck.html#t:HNNBlks">HNNBlks</a> o) o)<a href="src/Agda-Auto-Typecheck.html#hnn%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hnb" class="def">hnb</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o) o)<a href="src/Agda-Auto-Typecheck.html#hnb" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:HNRes" class="def">HNRes</a> o <a href="src/Agda-Auto-Typecheck.html#HNRes" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:HNDone" class="def">HNDone</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> (<a href="Agda-Auto-Syntax.html#t:Exp">Exp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o))) (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:HNMeta" class="def">HNMeta</a> (<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o) (<a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o) [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-Syntax.html#t:UId">UId</a> o)]</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:hnc" class="def">hnc</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-Syntax.html#t:UId">UId</a> o)] -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="Agda-Auto-Typecheck.html#t:HNRes">HNRes</a> o) o)<a href="src/Agda-Auto-Typecheck.html#hnc" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:hnarglist" class="def">hnarglist</a> :: <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="Agda-Auto-Syntax.html#t:HNArgList">HNArgList</a> o) o)<a href="src/Agda-Auto-Typecheck.html#hnarglist" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getNArgs" class="def">getNArgs</a> :: <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> ([<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o], <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o)) o)<a href="src/Agda-Auto-Typecheck.html#getNArgs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getAllArgs" class="def">getAllArgs</a> :: <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> [<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o] o)<a href="src/Agda-Auto-Typecheck.html#getAllArgs" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:PEval" class="def">PEval</a> o <a href="src/Agda-Auto-Typecheck.html#PEval" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:PENo" class="def">PENo</a> (<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:PEConApp" class="def">PEConApp</a> (<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o) (<a href="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</a> o) [<a href="Agda-Auto-Typecheck.html#t:PEval">PEval</a> o]</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:iotastep" class="def">iotastep</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyMB">MyMB</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> (<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o, <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o) (<a href="Agda-Auto-Typecheck.html#t:HNNBlks">HNNBlks</a> o)) o)<a href="src/Agda-Auto-Typecheck.html#iotastep" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:noiotastep" class="def">noiotastep</a> :: <a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#noiotastep" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:noiotastep_term" class="def">noiotastep_term</a> :: <a href="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</a> o -> <a href="Agda-Auto-Syntax.html#t:MArgList">MArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#noiotastep_term" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:CMode" class="def">CMode</a> o <a href="src/Agda-Auto-Typecheck.html#CMode" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:CMRigid" class="def">CMRigid</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> (<a href="Agda-Auto-Syntax.html#t:Exp">Exp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o))) (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><span class="keyword">forall</span> b . <a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> b (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o) => <a name="v:CMFlex" class="def">CMFlex</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> b (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)) (<a href="Agda-Auto-Typecheck.html#t:CMFlex">CMFlex</a> o)</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:CMFlex" class="def">CMFlex</a> o <a href="src/Agda-Auto-Typecheck.html#CMFlex" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:CMFFlex" class="def">CMFFlex</a> (<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o) (<a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o) [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-Syntax.html#t:UId">UId</a> o)]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CMFSemi" class="def">CMFSemi</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> (<a href="Agda-Auto-Syntax.html#t:Exp">Exp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o))) (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CMFBlocked" class="def">CMFBlocked</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> (<a href="Agda-Auto-Syntax.html#t:Exp">Exp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o))) (<a href="Agda-Auto-Syntax.html#t:HNExp">HNExp</a> o)</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:comp-39-" class="def">comp'</a> :: <span class="keyword">forall</span> o. <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-Auto-Syntax.html#t:CExp">CExp</a> o -> <a href="Agda-Auto-Syntax.html#t:CExp">CExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#comp%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:checkeliminand" class="def">checkeliminand</a> :: <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#checkeliminand" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:maybeor" class="def">maybeor</a> :: t -> t1 -> t2 -> t3 -> t2<a href="src/Agda-Auto-Typecheck.html#maybeor" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:iotapossmeta" class="def">iotapossmeta</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:ICArgList">ICArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</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-Auto-Typecheck.html#iotapossmeta" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:meta_not_constructor" class="def">meta_not_constructor</a> :: <a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o))<a href="src/Agda-Auto-Typecheck.html#meta_not_constructor" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:calcEqRState" class="def">calcEqRState</a> :: <a href="Agda-Auto-Syntax.html#t:EqReasoningConsts">EqReasoningConsts</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#calcEqRState" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:pickid" class="def">pickid</a> :: <a href="Agda-Auto-Syntax.html#t:MId">MId</a> -> <a href="Agda-Auto-Syntax.html#t:MId">MId</a> -> <a href="Agda-Auto-Syntax.html#t:MId">MId</a><a href="src/Agda-Auto-Typecheck.html#pickid" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:tcSearch" class="def">tcSearch</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> <a href="Agda-Auto-Syntax.html#t:Ctx">Ctx</a> o -> <a href="Agda-Auto-Syntax.html#t:CExp">CExp</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:EE">EE</a> (<a href="Agda-Auto-Syntax.html#t:MyPB">MyPB</a> o)<a href="src/Agda-Auto-Typecheck.html#tcSearch" class="link">Source</a></p></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>
