[Agda] An exercise in typing
effectfully at gmail.com
Mon Jun 13 15:08:11 CEST 2022
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.
More information about the Agda