<!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.SearchControl</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-SearchControl.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Auto-SearchControl.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.SearchControl</p></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:ExpRefInfo" class="def">ExpRefInfo</a> o <a href="src/Agda-Auto-SearchControl.html#ExpRefInfo" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:ExpRefInfo" class="def">ExpRefInfo</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:eriMain" class="def">eriMain</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:RefInfo">RefInfo</a> o)</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:eriUnifs" class="def">eriUnifs</a> :: [<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o]</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:eriInfTypeUnknown" class="def">eriInfTypeUnknown</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:eriIsEliminand" class="def">eriIsEliminand</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:eriUsedVars" class="def">eriUsedVars</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:UId">UId</a> o], [<a href="Agda-Auto-Syntax.html#t:Elr">Elr</a> o])</dt><dd class="doc empty"> </dd><dt class="src"><a name="v:eriIotaStep" class="def">eriIotaStep</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</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:eriPickSubsVar" class="def">eriPickSubsVar</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:eriEqRState" class="def">eriEqRState</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:EqReasoningState">EqReasoningState</a></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:getinfo" class="def">getinfo</a> :: [<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o] -> <a href="Agda-Auto-SearchControl.html#t:ExpRefInfo">ExpRefInfo</a> o<a href="src/Agda-Auto-SearchControl.html#getinfo" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:univar" class="def">univar</a> :: [<a href="Agda-Auto-Syntax.html#t:CAction">CAction</a> o] -> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</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:Nat">Nat</a><a href="src/Agda-Auto-SearchControl.html#univar" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:subsvars" class="def">subsvars</a> :: [<a href="Agda-Auto-Syntax.html#t:CAction">CAction</a> o] -> [<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>]<a href="src/Agda-Auto-SearchControl.html#subsvars" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:extraref" class="def">extraref</a> :: <a href="Agda-Auto-Syntax.html#t:UId">UId</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:ConstRef">ConstRef</a> o -> (<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/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> (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o)], <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="Agda-Auto-Syntax.html#t:Exp">Exp</a> o))<a href="src/Agda-Auto-SearchControl.html#extraref" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costIotaStep" class="def">costIotaStep</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-SearchControl.html#costIotaStep" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costIncrease" class="def">costIncrease</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-SearchControl.html#costIncrease" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppExtraRef" class="def">costAppExtraRef</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-SearchControl.html#costAppExtraRef" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costUnificationOccurs" class="def">costUnificationOccurs</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-SearchControl.html#costUnificationOccurs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costUnification" class="def">costUnification</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-SearchControl.html#costUnification" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppVar" class="def">costAppVar</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-SearchControl.html#costAppVar" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppVarUsed" class="def">costAppVarUsed</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-SearchControl.html#costAppVarUsed" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppHint" class="def">costAppHint</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-SearchControl.html#costAppHint" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppHintUsed" class="def">costAppHintUsed</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-SearchControl.html#costAppHintUsed" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppRecCall" class="def">costAppRecCall</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-SearchControl.html#costAppRecCall" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppRecCallUsed" class="def">costAppRecCallUsed</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-SearchControl.html#costAppRecCallUsed" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppConstructor" class="def">costAppConstructor</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-SearchControl.html#costAppConstructor" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAppConstructorSingle" class="def">costAppConstructorSingle</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-SearchControl.html#costAppConstructorSingle" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costLam" class="def">costLam</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-SearchControl.html#costLam" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costLamUnfold" class="def">costLamUnfold</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-SearchControl.html#costLamUnfold" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costPi" class="def">costPi</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-SearchControl.html#costPi" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costSort" class="def">costSort</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-SearchControl.html#costSort" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costInferredTypeUnkown" class="def">costInferredTypeUnkown</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-SearchControl.html#costInferredTypeUnkown" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAbsurdLam" class="def">costAbsurdLam</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-SearchControl.html#costAbsurdLam" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costEqStep" class="def">costEqStep</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-SearchControl.html#costEqStep" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costEqEnd" class="def">costEqEnd</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-SearchControl.html#costEqEnd" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costEqSym" class="def">costEqSym</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-SearchControl.html#costEqSym" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costEqCong" class="def">costEqCong</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-SearchControl.html#costEqCong" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioNo" class="def">prioNo</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-SearchControl.html#prioNo" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioAbsurdLambda" class="def">prioAbsurdLambda</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-SearchControl.html#prioAbsurdLambda" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioNoIota" class="def">prioNoIota</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-SearchControl.html#prioNoIota" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioCompCopy" class="def">prioCompCopy</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-SearchControl.html#prioCompCopy" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioCompUnif" class="def">prioCompUnif</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-SearchControl.html#prioCompUnif" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioCompChoice" class="def">prioCompChoice</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-SearchControl.html#prioCompChoice" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioCompIota" class="def">prioCompIota</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-SearchControl.html#prioCompIota" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioCompareArgList" class="def">prioCompareArgList</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-SearchControl.html#prioCompareArgList" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioCompBetaStructured" class="def">prioCompBetaStructured</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-SearchControl.html#prioCompBetaStructured" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioCompBeta" class="def">prioCompBeta</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-SearchControl.html#prioCompBeta" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioInferredTypeUnknown" class="def">prioInferredTypeUnknown</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-SearchControl.html#prioInferredTypeUnknown" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioTypecheckArgList" class="def">prioTypecheckArgList</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-SearchControl.html#prioTypecheckArgList" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioTypeUnknown" class="def">prioTypeUnknown</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-SearchControl.html#prioTypeUnknown" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioTypecheck" class="def">prioTypecheck</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Prelude.html#t:Num">Num</a> a => <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a> -> a<a href="src/Agda-Auto-SearchControl.html#prioTypecheck" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:prioProjIndex" class="def">prioProjIndex</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-SearchControl.html#prioProjIndex" 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>
