<!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.Interaction.MakeCase</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-Interaction-MakeCase.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-Interaction-MakeCase.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>None</td></tr></table><p class="caption">Agda.Interaction.MakeCase</p></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:CaseContext">CaseContext</a> <ul class="subs"><li>= <a href="#v:FunctionDef">FunctionDef</a> </li><li>| <a href="#v:ExtendedLambda">ExtendedLambda</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> </li></ul></li><li class="src short"><a href="#v:findClause">findClause</a> :: <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-Interaction-MakeCase.html#t:CaseContext">CaseContext</a>, <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a>)</li><li class="src short"><a href="#v:makeCase">makeCase</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a> -> <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-Interaction-MakeCase.html#t:CaseContext">CaseContext</a>, [<a href="Agda-Syntax-Abstract.html#t:Clause">Clause</a>])</li><li class="src short"><a href="#v:makeAbsurdClause">makeAbsurdClause</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Coverage.html#t:SplitClause">SplitClause</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Abstract.html#t:Clause">Clause</a></li><li class="src short"><a href="#v:makeAbstractClause">makeAbstractClause</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Coverage.html#t:SplitClause">SplitClause</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Abstract.html#t:Clause">Clause</a></li><li class="src short"><a href="#v:deBruijnIndex">deBruijnIndex</a> :: <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:CaseContext" class="def">CaseContext</a> <a href="src/Agda-Interaction-MakeCase.html#CaseContext" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:FunctionDef" class="def">FunctionDef</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:ExtendedLambda" class="def">ExtendedLambda</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></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:CaseContext" class="caption collapser" onclick="toggleSection('i:CaseContext')">Instances</p><div id="section.i:CaseContext" 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-Interaction-MakeCase.html#t:CaseContext">CaseContext</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:findClause" class="def">findClause</a> :: <a href="Agda-Syntax-Internal.html#t:MetaId">MetaId</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-Interaction-MakeCase.html#t:CaseContext">CaseContext</a>, <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a>, <a href="Agda-Syntax-Internal.html#t:Clause">Clause</a>)<a href="src/Agda-Interaction-MakeCase.html#findClause" class="link">Source</a></p><div class="doc"><p>Find the clause whose right hand side is the given meta
BY SEARCHING THE WHOLE SIGNATURE. Returns
the original clause, before record patterns have been translated
away. Raises an error if there is no matching clause.
</p><p>Andreas, 2010-09-21: This looks like a SUPER UGLY HACK to me. You are
walking through the WHOLE signature to find an information you have
thrown away earlier. (shutter with disgust).
This code fails for record rhs because they have been eta-expanded,
so the MVar is gone.
</p></div></div><div class="top"><p class="src"><a name="v:makeCase" class="def">makeCase</a> :: <a href="Agda-TypeChecking-Monad-Base.html#t:InteractionId">InteractionId</a> -> <a href="Agda-Syntax-Position.html#t:Range">Range</a> -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-String.html#t:String">String</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> (<a href="Agda-Interaction-MakeCase.html#t:CaseContext">CaseContext</a>, [<a href="Agda-Syntax-Abstract.html#t:Clause">Clause</a>])<a href="src/Agda-Interaction-MakeCase.html#makeCase" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:makeAbsurdClause" class="def">makeAbsurdClause</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Coverage.html#t:SplitClause">SplitClause</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Abstract.html#t:Clause">Clause</a><a href="src/Agda-Interaction-MakeCase.html#makeAbsurdClause" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:makeAbstractClause" class="def">makeAbstractClause</a> :: <a href="Agda-Syntax-Abstract-Name.html#t:QName">QName</a> -> <a href="Agda-TypeChecking-Coverage.html#t:SplitClause">SplitClause</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Abstract.html#t:Clause">Clause</a><a href="src/Agda-Interaction-MakeCase.html#makeAbstractClause" class="link">Source</a></p><div class="doc"><p>Make a clause with a question mark as rhs.
</p></div></div><div class="top"><p class="src"><a name="v:deBruijnIndex" class="def">deBruijnIndex</a> :: <a href="Agda-Syntax-Abstract.html#t:Expr">Expr</a> -> <a href="Agda-TypeChecking-Monad-Base.html#t:TCM">TCM</a> <a href="Agda-Syntax-Common.html#t:Nat">Nat</a><a href="src/Agda-Interaction-MakeCase.html#deBruijnIndex" 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>
