[Agda] An exercise in typing

[Ulf Norell]

Nice. Here's my solution:

https://gist.github.com/UlfNorell/aed09c281d1f6c515be4316a7a48874d

I found constructing the first argument to f in the recursive step to be
the trickiest part.

/ Ulf

On Sun, Jun 12, 2022 at 8:44 PM Roman <effectfully at gmail.com> wrote:

> Hi Jason.
>
> the body is the real challenge, `RecN` is a warm-up :)
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220613/2dc300f7/attachment.html>