<!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.CaseSplit</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-CaseSplit.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Auto-CaseSplit.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.CaseSplit</p></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:abspatvarname" class="def">abspatvarname</a> :: [<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Char.html#t:Char">Char</a>]<a href="src/Agda-Auto-CaseSplit.html#abspatvarname" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costCaseSplitVeryHigh" class="def">costCaseSplitVeryHigh</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-CaseSplit.html#costCaseSplitVeryHigh" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costCaseSplitHigh" class="def">costCaseSplitHigh</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-CaseSplit.html#costCaseSplitHigh" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costCaseSplitLow" class="def">costCaseSplitLow</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-CaseSplit.html#costCaseSplitLow" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:costAddVarDepth" class="def">costAddVarDepth</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-CaseSplit.html#costAddVarDepth" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:HI" class="def">HI</a> a <a href="src/Agda-Auto-CaseSplit.html#HI" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:HI" class="def">HI</a> <a href="Agda-Auto-Syntax.html#t:FMode">FMode</a> a</td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:drophid" class="def">drophid</a> :: [<a href="Agda-Auto-CaseSplit.html#t:HI">HI</a> b] -> [b]<a href="src/Agda-Auto-CaseSplit.html#drophid" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:CSPat" class="def">CSPat</a> o = <a href="Agda-Auto-CaseSplit.html#t:HI">HI</a> (<a href="Agda-Auto-CaseSplit.html#t:CSPatI">CSPatI</a> o)<a href="src/Agda-Auto-CaseSplit.html#CSPat" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:CSCtx" class="def">CSCtx</a> o = [<a href="Agda-Auto-CaseSplit.html#t:HI">HI</a> (<a href="Agda-Auto-Syntax.html#t:MId">MId</a>, <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o)]<a href="src/Agda-Auto-CaseSplit.html#CSCtx" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:CSPatI" class="def">CSPatI</a> o <a href="src/Agda-Auto-CaseSplit.html#CSPatI" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:CSPatConApp" class="def">CSPatConApp</a> (<a href="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</a> o) [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CSPatVar" class="def">CSPatVar</a> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CSPatExp" class="def">CSPatExp</a> (<a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CSWith" class="def">CSWith</a> (<a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o)</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CSAbsurd" class="def">CSAbsurd</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:CSOmittedArg" class="def">CSOmittedArg</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:Sol" class="def">Sol</a> o = [(<a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o, [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</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:MExp">MExp</a> o))]<a href="src/Agda-Auto-CaseSplit.html#Sol" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:caseSplitSearch" class="def">caseSplitSearch</a> :: <span class="keyword">forall</span> o. <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-Int.html#t:Int">Int</a> -> [<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-Maybe.html#t:Maybe">Maybe</a> (<a href="Agda-Auto-Syntax.html#t:EqReasoningConsts">EqReasoningConsts</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/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</a> o -> <a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> [<a href="Agda-Auto-CaseSplit.html#t:Sol">Sol</a> o]<a href="src/Agda-Auto-CaseSplit.html#caseSplitSearch" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:caseSplitSearch-39-" class="def">caseSplitSearch'</a> :: <span class="keyword">forall</span> o. (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Int.html#t:Int">Int</a> -> <a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> ([<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>], <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, [<a href="Agda-Auto-Syntax.html#t:Nat">Nat</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-Maybe.html#t:Maybe">Maybe</a> (<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-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="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</a> o -> <a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o] -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/System-IO.html#t:IO">IO</a> [<a href="Agda-Auto-CaseSplit.html#t:Sol">Sol</a> o]<a href="src/Agda-Auto-CaseSplit.html#caseSplitSearch%27" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:infertypevar" class="def">infertypevar</a> :: <a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o -> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o<a href="src/Agda-Auto-CaseSplit.html#infertypevar" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:replace" class="def">replace</a> :: <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o<a href="src/Agda-Auto-CaseSplit.html#replace" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:betareduce" class="def">betareduce</a> :: <a href="Agda-Auto-Syntax.html#t:MExp">MExp</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="src/Agda-Auto-CaseSplit.html#betareduce" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:concatargs" class="def">concatargs</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> (<a href="Agda-Auto-Syntax.html#t:ArgList">ArgList</a> o) (<a href="Agda-Auto-Syntax.html#t:RefInfo">RefInfo</a> o) -> <a href="Agda-Auto-Syntax.html#t:MArgList">MArgList</a> o -> <a href="Agda-Auto-Syntax.html#t:MArgList">MArgList</a> o<a href="src/Agda-Auto-CaseSplit.html#concatargs" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:eqelr" class="def">eqelr</a> :: <a href="Agda-Auto-Syntax.html#t:Elr">Elr</a> o -> <a href="Agda-Auto-Syntax.html#t:Elr">Elr</a> o -> <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-CaseSplit.html#eqelr" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:replacep" class="def">replacep</a> :: <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-CaseSplit.html#t:CSPatI">CSPatI</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o -> <a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o<a href="src/Agda-Auto-CaseSplit.html#replacep" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:rm" class="def">rm</a> :: <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a b -> a<a href="src/Agda-Auto-CaseSplit.html#rm" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mm" class="def">mm</a> :: a -> <a href="Agda-Auto-NarrowingSearch.html#t:MM">MM</a> a b<a href="src/Agda-Auto-CaseSplit.html#mm" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:unifyexp" class="def">unifyexp</a> :: <a href="Agda-Auto-Syntax.html#t:MExp">MExp</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-Maybe.html#t:Maybe">Maybe</a> [(<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o)]<a href="src/Agda-Auto-CaseSplit.html#unifyexp" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:lift" class="def">lift</a> :: <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o<a href="src/Agda-Auto-CaseSplit.html#lift" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:removevar" class="def">removevar</a> :: <a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o] -> [(<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o)] -> (<a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o, <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o, [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o])<a href="src/Agda-Auto-CaseSplit.html#removevar" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:notequal" class="def">notequal</a> :: <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</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/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-CaseSplit.html#notequal" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:findperm" class="def">findperm</a> :: [<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-Maybe.html#t:Maybe">Maybe</a> [<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>]<a href="src/Agda-Auto-CaseSplit.html#findperm" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:freevars" class="def">freevars</a> :: <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> [<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>]<a href="src/Agda-Auto-CaseSplit.html#freevars" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:applyperm" class="def">applyperm</a> :: [<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>] -> <a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o] -> (<a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o, <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o, [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o])<a href="src/Agda-Auto-CaseSplit.html#applyperm" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:ren" class="def">ren</a> :: <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> a => [a] -> 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-CaseSplit.html#ren" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:rename" class="def">rename</a> :: (<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>) -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o<a href="src/Agda-Auto-CaseSplit.html#rename" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:renamep" class="def">renamep</a> :: (<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>) -> <a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o -> <a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o<a href="src/Agda-Auto-CaseSplit.html#renamep" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:seqctx" class="def">seqctx</a> :: <a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o -> <a href="Agda-Auto-CaseSplit.html#t:CSCtx">CSCtx</a> o<a href="src/Agda-Auto-CaseSplit.html#seqctx" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:depthofvar" class="def">depthofvar</a> :: <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a> -> [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o] -> <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a><a href="src/Agda-Auto-CaseSplit.html#depthofvar" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:localTerminationEnv" class="def">localTerminationEnv</a> :: [<a href="Agda-Auto-CaseSplit.html#t:CSPat">CSPat</a> o] -> ([<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>], <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, [<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>])<a href="src/Agda-Auto-CaseSplit.html#localTerminationEnv" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:localTerminationSidecond" class="def">localTerminationSidecond</a> :: ([<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>], <a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>, [<a href="Agda-Auto-Syntax.html#t:Nat">Nat</a>]) -> <a href="Agda-Auto-Syntax.html#t:ConstRef">ConstRef</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-CaseSplit.html#localTerminationSidecond" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:getblks" class="def">getblks</a> :: <a href="Agda-Auto-Syntax.html#t:MExp">MExp</a> o -> <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:Nat">Nat</a>]<a href="src/Agda-Auto-CaseSplit.html#getblks" 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>
