[Agda] An exercise in typing

Ulf Norell ulf.norell at gmail.com
Mon Jun 13 13:34:46 CEST 2022

Nice. Here's my solution:


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>

More information about the Agda mailing list