[Agda] Re: Not understanding some goal solving stuff

[Chris Moline]

Ok, so I figured it out. Typical, struggle for awhile, give up and ask the
question, figure it out shortly after.

In the pdf there is a note that an implicit argument needs to be given. I
ignored it at the time because I didn't understand what was meant but then
it clicked. So where I had:

eq-plus-rec n m = natrec (refl m) (\ k' ih -> {! !}) n

I needed to have:

eq-plus-rec n m = natrec {\k -> (k + m) == (plus k m)} (refl m) (\ k' ih ->
{! !}) n

When I do this and then type 'c-c c-l'  a lot less text comes up. This is
cause giving the necessary argument explicitly solves a bunch of metas. I
didn't realize that's what they were but now I can complete the exercise.

Sorry for the noise.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140108/ae4778f4/attachment-0001.html