[Agda] Newbie questions after reading Dependently Typed Programming in Agda

[Ulf Norell]

On Tue, Oct 12, 2010 at 11:14 PM, Oscar Finnsson
<oscar.finnsson at gmail.com>wrote:

>
> 15. I cannot get the function "find" on p. 25 (Dependently Typed
> Programming in Agda) to compile.
> I get the error
> > F (p x) !=< T (not (p (_226 p xs npxs x prf))) of type Set
> > when checking that the expression falseIsFalse prf has type
> > T (not (p (_226 p xs npxs x prf)))
> regarding "falseIsFalse" on the last line in the function and I'm not
> knowledgeable enough in Agda to understand that error message.
> Not that it matters much, just thought someone (Ulf Norell?) might want to
> know.
>

The error message says that F (p x) is not the same as T (not (p x)), only
the second
x is the metavariable 226 which makes the error message a bit hard to
understand. I didn't
actually give the definition of isFalse (F in your code) in the tutorial
which I should have.
If you change your definition of F from

  F : Bool -> Set
  F true = False
  F false = True

to

  F : Bool -> Set
  F x = T (not x)

then the find type checks. Alternatively you can use the lemma

notFalseIsTrue : {x : Bool} -> x == false -> T (not x)
notFalseIsTrue refl = _

instead of falseIsFalse.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101013/bc7c0258/attachment.html