Expanding tactic macro

Stream: lean4

[Craig Disselkoen]

Hi, new here. I'm wondering, if I've written a tactic macro with macro_rules, is there a way to see what a particular invocation of it expands to?

[Alex J. Best]

You can use

  set_option trace.Elab.step true in
  my_macro

to see some info regarding this

[Craig Disselkoen]

Thanks for the tip!