testing tactics

Stream: general

[Scott Morrison]

I have a meta def T : expr → tactic expr := ... that I've written that isn't behaving properly, and I want to do some debugging. Inside the definition there are some trace statements that explain to me what's going on --- I just need a convenient way to invoke my tactic. Suppose I have some other def f := ..., and I want to invoke T on f. What do I do?

[Scott Morrison]

I'm hoping there's just something easy involving quotations that I don't know.

[Mario Carneiro]

Something like to_expr `(f) >>= T should work

[Scott Morrison]

term `(f) has type reflected f but is expected to have type pexpr

[Mario Carneiro]

Actually, `(f) is already an expr, so T `(f) should work

[Scott Morrison]

to_expr ``(f) works, however

[Mario Carneiro]

You would use to_expr if you need to parse the expression at run time rather than parse time

[Scott Morrison]

thanks!