<br><div class="gmail_quote">On Tue, Oct 12, 2010 at 11:14 PM, Oscar Finnsson <span dir="ltr"><<a href="mailto:oscar.finnsson@gmail.com">oscar.finnsson@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<br>
15. I cannot get the function "find" on p. 25 (Dependently Typed<br>
Programming in Agda) to compile.<br>
I get the error<br>
> F (p x) !=< T (not (p (_226 p xs npxs x prf))) of type Set<br>
> when checking that the expression falseIsFalse prf has type<br>
> T (not (p (_226 p xs npxs x prf)))<br>
regarding "falseIsFalse" on the last line in the function and I'm not<br>
knowledgeable enough in Agda to understand that error message.<br>
Not that it matters much, just thought someone (Ulf Norell?) might want to know.<br></blockquote><div><br></div><div>The error message says that F (p x) is not the same as T (not (p x)), only the second</div><div>x is the metavariable 226 which makes the error message a bit hard to understand. I didn't</div>
<div>actually give the definition of isFalse (F in your code) in the tutorial which I should have.</div><div>If you change your definition of F from</div><div><br></div><div> F : Bool -> Set</div><div> F true = False</div>
<div> F false = True</div><div><br></div><div>to </div><div><br></div><div> F : Bool -> Set</div><div> F x = T (not x)</div><div><br></div><div>then the find type checks. Alternatively you can use the lemma</div><div>
<br></div><div>notFalseIsTrue : {x : Bool} -> x == false -> T (not x)</div><div>notFalseIsTrue refl = _</div><div><br></div><div>instead of falseIsFalse.</div><div><br></div><div>/ Ulf</div></div>