<!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.NarrowingSearch</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-NarrowingSearch.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Auto-NarrowingSearch.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.NarrowingSearch</p></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Prio" class="def">Prio</a> = <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a><a href="src/Agda-Auto-NarrowingSearch.html#Prio" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:Trav" class="def">Trav</a> a blk | a -> blk <span class="keyword">where</span><a href="src/Agda-Auto-NarrowingSearch.html#Trav" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:traverse" class="def">traverse</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Control-Monad.html#t:Monad">Monad</a> m => (<span class="keyword">forall</span> b. <a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> b blk => <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> b blk -> m <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a>) -> a -> m <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Auto-NarrowingSearch.html#traverse" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:Trav" class="caption collapser" onclick="toggleSection('i:Trav')">Instances</p><div id="section.i:Trav" class="show"><table><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> a blk => <a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> [a] blk</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> (<a href="Agda-Auto-Syntax.html#t:ArgList">ArgList</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> (<a href="Agda-Auto-Syntax.html#t:Exp">Exp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> a blk => <a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk) blk</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> (<a href="Agda-Auto-Syntax.html#t:MId">MId</a>, <a href="Agda-Auto-Syntax.html#t:CExp">CExp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> (<a href="Agda-Auto-Syntax.html#t:TrBr">TrBr</a> a o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Term" class="def">Term</a> blk <a href="src/Agda-Auto-NarrowingSearch.html#Term" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><span class="keyword">forall</span> a . <a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> a blk => <a name="v:Term" class="def">Term</a> a</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Prop" class="def">Prop</a> blk <a href="src/Agda-Auto-NarrowingSearch.html#Prop" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:OK" class="def">OK</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Error" class="def">Error</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr><tr><td class="src"><span class="keyword">forall</span> a . <a name="v:AddExtraRef" class="def">AddExtraRef</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a blk) (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>, <a href="Agda-Auto-NarrowingSearch.html#t:RefCreateEnv">RefCreateEnv</a> blk a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:And" class="def">And</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:Term">Term</a> blk]) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk))</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Sidecondition" class="def">Sidecondition</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk))</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Or" class="def">Or</a> <a href="Agda-Auto-NarrowingSearch.html#t:Prio">Prio</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk))</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:ConnectHandle" class="def">ConnectHandle</a> (<a href="Agda-Auto-NarrowingSearch.html#t:OKHandle">OKHandle</a> blk) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk))</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:OKVal" class="def">OKVal</a> <a href="src/Agda-Auto-NarrowingSearch.html#OKVal" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:OKVal" class="def">OKVal</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:OKVal" class="caption collapser" onclick="toggleSection('i:OKVal')">Instances</p><div id="section.i:OKVal" class="show"><table><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> <a href="Agda-Auto-NarrowingSearch.html#t:OKVal">OKVal</a> blk</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:OKHandle" class="def">OKHandle</a> blk = <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> <a href="Agda-Auto-NarrowingSearch.html#t:OKVal">OKVal</a> blk<a href="src/Agda-Auto-NarrowingSearch.html#OKHandle" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:OKMeta" class="def">OKMeta</a> blk = <a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> <a href="Agda-Auto-NarrowingSearch.html#t:OKVal">OKVal</a> blk<a href="src/Agda-Auto-NarrowingSearch.html#OKMeta" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Metavar" class="def">Metavar</a> a blk <a href="src/Agda-Auto-NarrowingSearch.html#Metavar" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Metavar" class="def">Metavar</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:mbind" class="def">mbind</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:mprincipalpresent" class="def">mprincipalpresent</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:mobs" class="def">mobs</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> [(<a href="Agda-Auto-NarrowingSearch.html#t:QPB">QPB</a> a blk, <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:CTree">CTree</a> blk))]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:mcompoint" class="def">mcompoint</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> [<a href="Agda-Auto-NarrowingSearch.html#t:SubConstraints">SubConstraints</a> blk]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:mextrarefs" class="def">mextrarefs</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</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-NarrowingSearch.html#t:RefCreateEnv">RefCreateEnv</a> blk a)]</dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div><div class="subs instances"><p id="control.i:Metavar" class="caption collapser" onclick="toggleSection('i:Metavar')">Instances</p><div id="section.i:Metavar" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a blk)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:hequalMetavar" class="def">hequalMetavar</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a1 blk1 -> <a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a2 bkl2 -> <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-NarrowingSearch.html#hequalMetavar" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:newMeta" class="def">newMeta</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> [<a href="Agda-Auto-NarrowingSearch.html#t:SubConstraints">SubConstraints</a> blk] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a blk)<a href="src/Agda-Auto-NarrowingSearch.html#newMeta" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:initMeta" class="def">initMeta</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a blk)<a href="src/Agda-Auto-NarrowingSearch.html#initMeta" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:CTree" class="def">CTree</a> blk <a href="src/Agda-Auto-NarrowingSearch.html#CTree" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:CTree" class="def">CTree</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:ctpriometa" class="def">ctpriometa</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PrioMeta">PrioMeta</a> blk)</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:ctsub" class="def">ctsub</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</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:SubConstraints">SubConstraints</a> blk))</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:ctparent" class="def">ctparent</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</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:CTree">CTree</a> blk))</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:cthandles" class="def">cthandles</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> [<a href="Agda-Auto-NarrowingSearch.html#t:OKMeta">OKMeta</a> blk]</dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:SubConstraints" class="def">SubConstraints</a> blk <a href="src/Agda-Auto-NarrowingSearch.html#SubConstraints" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:SubConstraints" class="def">SubConstraints</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:scflip" class="def">scflip</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:sccomcount" class="def">sccomcount</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a></dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scsub1" class="def">scsub1</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:CTree">CTree</a> blk</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:scsub2" class="def">scsub2</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:CTree">CTree</a> blk</dt><dd class="doc empty"> </dd></dl><div class="clear"></div></div></td></tr></table></div></div><div class="top"><p class="src"><a name="v:newCTree" class="def">newCTree</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:CTree">CTree</a> blk) -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> (<a href="Agda-Auto-NarrowingSearch.html#t:CTree">CTree</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#newCTree" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:newSubConstraints" class="def">newSubConstraints</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:CTree">CTree</a> blk -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> (<a href="Agda-Auto-NarrowingSearch.html#t:SubConstraints">SubConstraints</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#newSubConstraints" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:PrioMeta" class="def">PrioMeta</a> blk <a href="src/Agda-Auto-NarrowingSearch.html#PrioMeta" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><span class="keyword">forall</span> a . <a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> a blk => <a name="v:PrioMeta" class="def">PrioMeta</a> <a href="Agda-Auto-NarrowingSearch.html#t:Prio">Prio</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a blk)</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:NoPrio" class="def">NoPrio</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:PrioMeta" class="caption collapser" onclick="toggleSection('i:PrioMeta')">Instances</p><div id="section.i:PrioMeta" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PrioMeta">PrioMeta</a> blk)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Restore" class="def">Restore</a> <a href="src/Agda-Auto-NarrowingSearch.html#Restore" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><span class="keyword">forall</span> a . <a name="v:Restore" class="def">Restore</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> a) a</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Undo" class="def">Undo</a> = <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Lazy.html#t:StateT">StateT</a> [<a href="Agda-Auto-NarrowingSearch.html#t:Restore">Restore</a>] <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a><a href="src/Agda-Auto-NarrowingSearch.html#Undo" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:ureadIORef" class="def">ureadIORef</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> a -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</a> a<a href="src/Agda-Auto-NarrowingSearch.html#ureadIORef" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:uwriteIORef" class="def">uwriteIORef</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> a -> a -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Auto-NarrowingSearch.html#uwriteIORef" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:umodifyIORef" class="def">umodifyIORef</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> a -> (a -> a) -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Auto-NarrowingSearch.html#umodifyIORef" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:ureadmodifyIORef" class="def">ureadmodifyIORef</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> a -> (a -> a) -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</a> a<a href="src/Agda-Auto-NarrowingSearch.html#ureadmodifyIORef" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:runUndo" class="def">runUndo</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</a> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> a<a href="src/Agda-Auto-NarrowingSearch.html#runUndo" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:RefCreateEnv" class="def">RefCreateEnv</a> blk = <a href="/usr/share/doc/ghc/html/libraries/mtl-2.1.2/Control-Monad-State-Lazy.html#t:StateT">StateT</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> [<a href="Agda-Auto-NarrowingSearch.html#t:SubConstraints">SubConstraints</a> blk], <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a>) <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a><a href="src/Agda-Auto-NarrowingSearch.html#RefCreateEnv" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Pair" class="def">Pair</a> a b <a href="src/Agda-Auto-NarrowingSearch.html#Pair" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:Pair" class="def">Pair</a> a b</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:Refinable" class="def">Refinable</a> a blk | a -> blk <span class="keyword">where</span><a href="src/Agda-Auto-NarrowingSearch.html#Refinable" class="link">Source</a></p><div class="subs methods"><p class="caption">Methods</p><p class="src"><a name="v:refinements" class="def">refinements</a> :: blk -> [blk] -> <a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a blk -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</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-NarrowingSearch.html#t:RefCreateEnv">RefCreateEnv</a> blk a)]<a href="src/Agda-Auto-NarrowingSearch.html#refinements" class="link">Source</a></p></div><div class="subs instances"><p id="control.i:Refinable" class="caption collapser" onclick="toggleSection('i:Refinable')">Instances</p><div id="section.i:Refinable" class="show"><table><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> <a href="Agda-Auto-NarrowingSearch.html#t:Choice">Choice</a> blk</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> <a href="Agda-Auto-NarrowingSearch.html#t:OKVal">OKVal</a> blk</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> (<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> (<a href="Agda-Auto-Syntax.html#t:ArgList">ArgList</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> (<a href="Agda-Auto-Syntax.html#t:Exp">Exp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> (<a href="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:newPlaceholder" class="def">newPlaceholder</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:RefCreateEnv">RefCreateEnv</a> blk (<a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk)<a href="src/Agda-Auto-NarrowingSearch.html#newPlaceholder" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:newOKHandle" class="def">newOKHandle</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:RefCreateEnv">RefCreateEnv</a> blk (<a href="Agda-Auto-NarrowingSearch.html#t:OKHandle">OKHandle</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#newOKHandle" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:dryInstantiate" class="def">dryInstantiate</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:RefCreateEnv">RefCreateEnv</a> blk a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> a<a href="src/Agda-Auto-NarrowingSearch.html#dryInstantiate" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:BlkInfo" class="def">BlkInfo</a> blk = (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a>, <a href="Agda-Auto-NarrowingSearch.html#t:Prio">Prio</a>, <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#BlkInfo" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:MM" class="def">MM</a> a blk <a href="src/Agda-Auto-NarrowingSearch.html#MM" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NotM" class="def">NotM</a> a</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Meta" class="def">Meta</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a blk)</td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:MM" class="caption collapser" onclick="toggleSection('i:MM')">Instances</p><div id="section.i:MM" class="show"><table><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> (<a href="Agda-Auto-Syntax.html#t:ICExp">ICExp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> a blk => <a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk) blk</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Trav">Trav</a> (<a href="Agda-Auto-Syntax.html#t:MId">MId</a>, <a href="Agda-Auto-Syntax.html#t:CExp">CExp</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:MetaEnv" class="def">MetaEnv</a> = <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a><a href="src/Agda-Auto-NarrowingSearch.html#MetaEnv" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:MB" class="def">MB</a> a blk <a href="src/Agda-Auto-NarrowingSearch.html#MB" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NotB" class="def">NotB</a> a</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 blk => <a name="v:Blocked" class="def">Blocked</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> b blk) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> a blk))</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Failed" class="def">Failed</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:PB" class="def">PB</a> blk <a href="src/Agda-Auto-NarrowingSearch.html#PB" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NotPB" class="def">NotPB</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Prop">Prop</a> blk)</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 blk => <a name="v:PBlocked" class="def">PBlocked</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> b blk) (<a href="Agda-Auto-NarrowingSearch.html#t:BlkInfo">BlkInfo</a> blk) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk))</td><td class="doc empty"> </td></tr><tr><td class="src"><span class="keyword">forall</span> b1 b2 . (<a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> b1 blk, <a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> b2 blk) => <a name="v:PDoubleBlocked" class="def">PDoubleBlocked</a> (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> b1 blk) (<a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> b2 blk) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk))</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:QPB" class="def">QPB</a> b blk <a href="src/Agda-Auto-NarrowingSearch.html#QPB" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:QPBlocked" class="def">QPBlocked</a> (<a href="Agda-Auto-NarrowingSearch.html#t:BlkInfo">BlkInfo</a> blk) (<a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk))</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:QPDoubleBlocked" class="def">QPDoubleBlocked</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</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-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk))</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:mmcase" class="def">mmcase</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> a blk => <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk -> (a -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk)) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk)<a href="src/Agda-Auto-NarrowingSearch.html#mmcase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mmmcase" class="def">mmmcase</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> a blk => <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk) -> (a -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk)) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk)<a href="src/Agda-Auto-NarrowingSearch.html#mmmcase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mmpcase" class="def">mmpcase</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> a blk => <a href="Agda-Auto-NarrowingSearch.html#t:BlkInfo">BlkInfo</a> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk -> (a -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#mmpcase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:doubleblock" class="def">doubleblock</a> :: (<a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> a blk, <a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> b blk) => <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> b blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#doubleblock" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mbcase" class="def">mbcase</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> a blk) -> (a -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk)) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk)<a href="src/Agda-Auto-NarrowingSearch.html#mbcase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mbpcase" class="def">mbpcase</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Prio">Prio</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> a blk) -> (a -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#mbpcase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mmbpcase" class="def">mmbpcase</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> a blk) -> (<span class="keyword">forall</span> b. <a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> b blk => <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> b blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)) -> (a -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#mmbpcase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:waitok" class="def">waitok</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:OKHandle">OKHandle</a> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> b blk)<a href="src/Agda-Auto-NarrowingSearch.html#waitok" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mbret" class="def">mbret</a> :: a -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> a blk)<a href="src/Agda-Auto-NarrowingSearch.html#mbret" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mbfailed" class="def">mbfailed</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MB">MB</a> a blk)<a href="src/Agda-Auto-NarrowingSearch.html#mbfailed" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mpret" class="def">mpret</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Prop">Prop</a> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#mpret" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:expandbind" class="def">expandbind</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a blk)<a href="src/Agda-Auto-NarrowingSearch.html#expandbind" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:HandleSol" class="def">HandleSol</a> = <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> <a href="/usr/share/doc/ghc/html/libraries/ghc-prim-0.2.0.0/GHC-Tuple.html#t:-40--41-">()</a><a href="src/Agda-Auto-NarrowingSearch.html#HandleSol" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:SRes" class="def">SRes</a> = <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Either.html#t:Either">Either</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a><a href="src/Agda-Auto-NarrowingSearch.html#SRes" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:topSearch" class="def">topSearch</a> :: <span class="keyword">forall</span> blk. <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</a> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-IORef.html#t:IORef">IORef</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-NarrowingSearch.html#t:HandleSol">HandleSol</a> -> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk) -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</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-NarrowingSearch.html#topSearch" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:extractblkinfos" class="def">extractblkinfos</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Metavar">Metavar</a> a blk -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> [blk]<a href="src/Agda-Auto-NarrowingSearch.html#extractblkinfos" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:recalcs" class="def">recalcs</a> :: [(<a href="Agda-Auto-NarrowingSearch.html#t:QPB">QPB</a> a blk, <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:CTree">CTree</a> blk))] -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</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-NarrowingSearch.html#recalcs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:seqc" class="def">seqc</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</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-NarrowingSearch.html#t:Undo">Undo</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-NarrowingSearch.html#t:Undo">Undo</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-NarrowingSearch.html#seqc" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:recalc" class="def">recalc</a> :: (<a href="Agda-Auto-NarrowingSearch.html#t:QPB">QPB</a> a blk, <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:CTree">CTree</a> blk)) -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</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-NarrowingSearch.html#recalc" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:reccalc" class="def">reccalc</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk) -> <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:CTree">CTree</a> blk) -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</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-NarrowingSearch.html#reccalc" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:calc" class="def">calc</a> :: <span class="keyword">forall</span> blk. <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk) -> <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:CTree">CTree</a> blk) -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</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:OKMeta">OKMeta</a> blk])<a href="src/Agda-Auto-NarrowingSearch.html#calc" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:choosePrioMeta" class="def">choosePrioMeta</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-NarrowingSearch.html#t:PrioMeta">PrioMeta</a> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:PrioMeta">PrioMeta</a> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:PrioMeta">PrioMeta</a> blk<a href="src/Agda-Auto-NarrowingSearch.html#choosePrioMeta" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:propagatePrio" class="def">propagatePrio</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:CTree">CTree</a> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:Undo">Undo</a> [<a href="Agda-Auto-NarrowingSearch.html#t:OKMeta">OKMeta</a> blk]<a href="src/Agda-Auto-NarrowingSearch.html#propagatePrio" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Choice" class="def">Choice</a> <a href="src/Agda-Auto-NarrowingSearch.html#Choice" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:LeftDisjunct" class="def">LeftDisjunct</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:RightDisjunct" class="def">RightDisjunct</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Choice" class="caption collapser" onclick="toggleSection('i:Choice')">Instances</p><div id="section.i:Choice" class="show"><table><tr><td class="src"><a href="Agda-Auto-NarrowingSearch.html#t:Refinable">Refinable</a> <a href="Agda-Auto-NarrowingSearch.html#t:Choice">Choice</a> blk</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:choose" class="def">choose</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> <a href="Agda-Auto-NarrowingSearch.html#t:Choice">Choice</a> blk -> <a href="Agda-Auto-NarrowingSearch.html#t:Prio">Prio</a> -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk) -> <a href="Agda-Auto-NarrowingSearch.html#t:MetaEnv">MetaEnv</a> (<a href="Agda-Auto-NarrowingSearch.html#t:PB">PB</a> blk)<a href="src/Agda-Auto-NarrowingSearch.html#choose" 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>
