[Agda] Reflection + monoiddsolver

[Ulf Norell]

I have a solver in agda-prelude that might work:

https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Monoid.agda
https://github.com/UlfNorell/agda-prelude/blob/master/test/MonoidTactic.agda

/ Ulf

On Fri, Nov 22, 2019 at 4:32 PM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Hi,
>
>
>
> A student of mine has to prove equations over lists with append and this
> becomes very cumbersome quickly. What is the current status of using a
> monoid solver and relfection?
>
>
>
> Thorsten
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> _______________________________________________
> 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/20191122/23eb571a/attachment.html>