[Agda] An exercise in typing

[Arseniy Alekseyev]

An "object-oriented" [1] solution:

https://gist.github.com/Rotsor/136dd9585b73495c7fd27d6d415b15b4

(still using lists, so doesn't solve the "hard" problem)

[1] Object = Σ Set (λ A → A)
:-)

On Tue, 21 Jun 2022 at 03:05, Roman <effectfully at gmail.com> wrote:

> It's been a week, so here's my solution that recurses on `n` once at
> the term level:
> https://gist.github.com/effectfully/790fe6549a0ccc519bda4b9680b63b67
>
> Hope it was a funny little puzzle.
> _______________________________________________
> 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/20220626/e7b02732/attachment.html>