[Agda] Info about instance resolution in macro

[Ulf Norell]

Interaction between instance search and tactics is currently a little
flaky. Could you add your problem to this issue:

https://github.com/agda/agda/issues/4777

I believe the problem in your case is that instance search runs after the
macro, and there's currently no way to force it
to happen during the macro call.

/ Ulf

On Tue, Sep 15, 2020 at 7:15 PM Joris Ceulemans <joris.ceulemans at vub.be>
wrote:

> Hello,
>
>
> When defining a macro, is it possible to get information on whether
> instance resolution for a specific instance metavariable succeeds or not
> and based on that do different things?
>
> Attached is a small example of what I have in mind. I tried working with
> "noConstraints" but that doesn't work (or at least not the way that I
> use it).
>
>
> Best,
>
> Joris
>
> _______________________________________________
> 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/20200916/dcc65e9e/attachment.html>