[Agda] An exercise in typing

[Ulf Norell]

Ah, nice. You actually only need `const` in mapForallN. When I realised I
needed it I added it
where it would provide the most power :-)

/ Ulf

On Mon, Jun 13, 2022 at 3:08 PM Roman <effectfully at gmail.com> wrote:

> Ulf, that's a cool solution.
>
> I simplified it a little by dropping the second argument from
> `forallN`:
> https://gist.github.com/effectfully/dab7fd1ad7c15d81d386f1aef6632725
>
> (it doesn't really simplify the logic, just the appearance)
>
> If you feel like doing another version of the challenge, it's possible
> to solve it by recursing on `n` only once at the term level, rather
> than twice in quadratic fashion (you do `mapForallN n` at each
> recursive step). Not that it matters though.
>
> Great solution!
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220613/dd998242/attachment.html>