Zulip Chat Archive

Stream: general

Topic: testing tactics


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:06):

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

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:07):

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

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:09):

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

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:09):

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

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:09):

to_expr ``(f) works, however

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:10):

thanks!


Last updated: May 12 2021 at 03:23 UTC