[Agda] Examples of tacticts via reflection

[Andrej Bauer]

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