how to debug a macro

Stream: new members

[ZHAO Jiecheng]

I am learning macro, but when It throws errors, I still don't know what was happened. Is there any way that I can read the text generated by the macro generated (even it is illegal)?

[Mario Carneiro]

not very easily, but you can see the macro expansion trace in set_option trace.Elab.info true output

[ZHAO Jiecheng]

Mario Carneiro said:

not very easily, but you can see the macro expansion trace in set_option trace.Elab.info true output

It looks like too much info in the trace. As I am not familiar with macro, I may need something more clean and helpful.

[Alex J. Best]

A #mwe would be helpful here, so we can see better what sort of macro's you have