<div dir="ltr">Ok, so I figured it out. Typical, struggle for awhile, give up and ask the question, figure it out shortly after.<div><br></div><div>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:</div>
<div><br></div><div>eq-plus-rec n m = natrec (refl m) (\ k' ih -> {! !}) n</div><div><br></div><div>I needed to have:</div><div><br></div><div>eq-plus-rec n m = natrec {\k -> (k + m) == (plus k m)} (refl m) (\ k' ih -> {! !}) n</div>
<div><br></div><div>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. </div>
<div><br></div><div>Sorry for the noise.</div></div>