<p><span class="h-card" translate="no"><a href="https://ublog.thirdlaw.net/users/sree" class="u-url mention">@<span>sree</span></a></span> <span class="h-card" translate="no"><a href="https://hachyderm.io/@unlambda" class="u-url mention">@<span>unlambda</span></a></span> <span class="h-card" translate="no"><a href="https://mastodon.social/@regehr" class="u-url mention">@<span>regehr</span></a></span> <span class="h-card" translate="no"><a href="https://types.pl/@lenary" class="u-url mention">@<span>lenary</span></a></span> the way loops go is that i start with a base case (reset state) and for every possible input vector, output vector must be the same between two functions i'm considering</p><p>unrolling it won't work, i need induction if i'm to get anywhere, i think</p>