<br><br><div class="gmail_quote">2010/2/19 Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im"><br></div>
The connection of our problem to the one in the thread is not apparent. Here is a rephrasement of the problem, not using dot patterns.<br>
<br>
f : {n m : Nat} -> D n (suc m) -> Nat<br>
f (c (suc i) zero) = bla -- FAILS already<br>
f (c i (suc zero)) = bla<br>
f (c zero zero)<br></blockquote><blockquote class="gmail_quote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; ">
<br></blockquote><blockquote class="gmail_quote" style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; ">
How would I write a series of patterns for f that do type-check?</blockquote><div><br></div><div>Here's how you do it:</div><div><br></div><div>f′ : {n m′ m : Nat} -> D n m′ -> m′ ≡ suc m -> Nat</div><div>f′ (c (suc i) zero) refl = bla</div>
<div>f′ (c i (suc zero)) refl = bla</div><div>f′ (c i (suc (suc d))) refl = {!you missed this case!}</div><div>f′ (c zero zero) ()</div><div><br></div><div>f : {n m : Nat} -> D n (suc m) -> Nat</div><div>f d = f′ d refl</div>
<div><br></div><div>The reason your version is not accepted is that the type checking algorithm requires that each function definition corresponds to a (type correct) case splitting tree. Basically, if you can't C-c C-c your way to the definition it won't be accepted. In your example</div>
<div><br></div><div> f (c i d) = ?</div><div><br></div><div>is not a valid refinement of the problem f x = ? (since d + i doesn't unify with suc m).</div><div><br></div><div>/ Ulf</div></div>