<div dir="ltr"><div>Hello again,</div><div><br></div><div>The second part of my blog series on rewrite rules in Agda is now online: <a href="https://jesper.sikanda.be/posts/rewriting-type-theory.html">https://jesper.sikanda.be/posts/rewriting-type-theory.html</a>. This time I go into the nitty-gritty details of how rewrite rules work and how they interact with other features of Agda. Comments are very welcome as usual!</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Oct 21, 2019 at 3:22 PM Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</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"><div dir="ltr"><div>Hi Agda folks,</div><div><br></div><div>I have another blog post for you on extending Agda with rewrite rules, with no less than six examples of how they can be used. You can read it at <a href="https://jesper.sikanda.be/posts/hack-your-type-theory.html" target="_blank">https://jesper.sikanda.be/posts/hack-your-type-theory.html</a>. Any comments are welcome here on the mailing list as usual.</div><div><br></div><div>Cheers,</div><div>Jesper<br></div></div>
</blockquote></div>