## Stream: general

### Topic: testing tactics

#### Scott Morrison (Mar 16 2018 at 10:06):

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 (Mar 16 2018 at 10:06):

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

#### Mario Carneiro (Mar 16 2018 at 10:07):

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

#### Scott Morrison (Mar 16 2018 at 10:09):

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

#### Mario Carneiro (Mar 16 2018 at 10:09):

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

#### Scott Morrison (Mar 16 2018 at 10:09):

 to_expr (f) works, however

#### Mario Carneiro (Mar 16 2018 at 10:09):

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

#### Scott Morrison (Mar 16 2018 at 10:10):

thanks!

Last updated: May 12 2021 at 03:23 UTC