<div dir="ltr"><div><div>I don't have much to say about exposing rewrite to the reflection, but I do have a warning: the module Agda.TypeChecking.Rewriting is *not* for checking functions that use the 'rewrite' keyword, but rather for a new (and experimental) feature for adding user-defined rewrite rules to the evaluator via {-# REWRITE ... #-} pragmas. For the code handling the 'rewrite' keyword, you can take a look at the checkRHS function in Agda.TypeChecking.Rules.Def.<br><br></div>cheers,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 31, 2016 at 8:53 PM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Via reflection, it currently isn't straightforward to construct an agda function that invokes a rewrite. Exposing Agda's rewriting machinery to reflection would make this much easier. (Another neat idea is to expose agsy!) On the other hand, the exact same algorithms could be reproduced in the Agda language and it might be advisable to keep the reflection interface clean, especially considering that work done by "rewrite" or agsy might change in the future.<br><br>Am I correct that Agda.TypeChecking.Rewriting can now be exactly
reproduced in Agda? I'm studying the algorithm and would love to know
that the path ahead of me is clear.<br>--<br></div><div><div><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">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>
<br></blockquote></div><br></div>