[Agda] Examples of tacticts via reflection

[Patrik Jansson]

Andrej Bauer skrev:
> Dear Agdaists,
>
> I am new to Agda and I am looking for examples of how to implement and
> use in Agda something similar to Coq's tactics. As I understand it,
> the idea is to use reflection and universes. Where can I see some
> examples, such as computing the normal form of a polynomial, or
> checking the truth of a boolean proposition by truth-tables? 
One example in the Agda libs is the ring solver:
http://www.cs.nott.ac.uk/~nad/listings/lib/Algebra.RingSolver.html

/Patrik



> What
> about "tactics" that may fail or succeed, are there libraries to
> combine those?
>
> Thanks,
>
> Andrej
>
> P.S. I suspect many users of Coq come to the Agda wiki to see what it
> is about. It would be great if there were a page for them, explaining
> the similarities and the differences.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>