<div dir="ltr"><div>Please help me figure out why I'm getting unsolved metas <a href="https://github.com/m0davis/agda-prelude/blob/WIP/test/Reright.agda">here</a>, from <a href="https://github.com/m0davis/agda-prelude/commit/c013e56ac9a8b7b7d986dc27d67e24f1a614d026">my fork of agda-prelude</a>.<br><br>'reright' is intended to work just like rewrite, except it's invokable from the rhs. From my extensive testing, it seems to work as one would want and expect: it provides rewritten context variables and rewrites the goal in a manner equivalent to 'rewrite'. However, it has trouble sometimes when a reright is nested within another reright: that's where I'm getting unsolved metas. Afaics, the inner reright blocksOnMeta, then the outer reright
completes and the computation wrt the inner reright never gets
restarted. Beyond that, I'm not sure why or what to do about it.<br></div><div><br></div>NB, I'm aware of how horribly-written the code is. I fully intend a major refactor as soon as I work through the bugs!<br clear="all"><div><div><div><div class="gmail_signature"><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">--<br>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></div>