[Agda] [reright] debugging unsolved metas in a nested tactic

[Martin Stone Davis]

Please help me figure out why I'm getting unsolved metas here
<https://github.com/m0davis/agda-prelude/blob/WIP/test/Reright.agda>, from my
fork of agda-prelude
<https://github.com/m0davis/agda-prelude/commit/c013e56ac9a8b7b7d986dc27d67e24f1a614d026>
.

'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.

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!
--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160224/38029ff6/attachment.html