Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Registering a new option


view this post on Zulip Jannis Limperg (Jul 20 2020 at 14:45):

I'd like to have a trace.eliminate_hyp option for my elimination tactic so that one can write

set_options trace.eliminate_hyp true

and get a trace when eliminate_hyp is called. However, when called as above,set_options says 'unknown option'. Can I register trace.eliminate_hyp as a settable option?

view this post on Zulip Rob Lewis (Jul 20 2020 at 14:47):

Use the command declare_trace eliminate_hyp.

view this post on Zulip Rob Lewis (Jul 20 2020 at 14:47):

You can access it with tactic.when_tracing `eliminate_hyp

view this post on Zulip Jannis Limperg (Jul 20 2020 at 14:49):

Awesome, thank you!

view this post on Zulip Scott Morrison (Jul 21 2020 at 01:27):

There's also trace_if_enabled `eliminate_hyp "message".


Last updated: May 09 2021 at 23:10 UTC