[Agda] New blog post: Hack your type theory with rewrite rules

[Apostolis Xekoukoulotakis]

If you have proved the equality as in your 2nd example, is there any reason
not to use REWRITE?
My impression is that I should use REWRITE everywhere where I have proven a
propositional equality so as to make it definitional.

Nice blog post, and a good reference to a book on type theory. I was
looking into a good introductory book that would help me understand agda a
bit better.

On Mon, Oct 21, 2019 at 4:22 PM Jesper Cockx <Jesper at sikanda.be> wrote:

> Hi Agda folks,
>
> 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
> https://jesper.sikanda.be/posts/hack-your-type-theory.html. Any comments
> are welcome here on the mailing list as usual.
>
> Cheers,
> Jesper
> _______________________________________________
> 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/20191021/bdf1f009/attachment.html>