<div dir="ltr"><div>An "object-oriented" [1] solution: <br></div><div><br></div><div><a href="https://gist.github.com/Rotsor/136dd9585b73495c7fd27d6d415b15b4">https://gist.github.com/Rotsor/136dd9585b73495c7fd27d6d415b15b4</a></div><div><br></div><div>(still using lists, so doesn't solve the "hard" problem)<br></div><div><br></div><div>[1] Object = Σ Set (λ A → A) <br></div><div>:-)<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 21 Jun 2022 at 03:05, Roman <<a href="mailto:effectfully@gmail.com">effectfully@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">It's been a week, so here's my solution that recurses on `n` once at<br>
the term level:<br>
<a href="https://gist.github.com/effectfully/790fe6549a0ccc519bda4b9680b63b67" rel="noreferrer" target="_blank">https://gist.github.com/effectfully/790fe6549a0ccc519bda4b9680b63b67</a><br>
<br>
Hope it was a funny little puzzle.<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>