[Agda] An exercise in typing
ulf.norell at gmail.com
Mon Jun 13 15:16:37 CEST 2022
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 :-)
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
> (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...
More information about the Agda