[Agda] Reflection + monoiddsolver

[Jesper Cockx]

There is also a reflection-based monoid solver available in the
experimental branch of the standard library:
https://github.com/agda/agda-stdlib/blob/experimental/README/Solvers/ReflectiveMonoid.agda
(I haven't used it yet myself).

-- Jesper

On Fri, Nov 22, 2019 at 4:41 PM Ulf Norell <ulf.norell at gmail.com> wrote:

> 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
>>
> _______________________________________________
> 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/dcc24a4c/attachment.html>