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

[Martin Stone Davis]

A thought on how I might make progress: I'm missing information that would
be helpful to debugging this. I suspect that the metavariable, _N, sent to
blockOnMeta in the inner call to reright needs to then be solved somehow by
the computation in the outer call. However, I can't see what _N is or how
it might be connected to other metavariables, and so I can't tell why it
isn't getting solved. Is there some way to see these behind-the-scenes
details?

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

On Wed, Feb 24, 2016 at 12:40 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> 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/42b60ba7/attachment.html