Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Registering a new option


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?

Rob Lewis (Jul 20 2020 at 14:47):

Use the command declare_trace eliminate_hyp.

Rob Lewis (Jul 20 2020 at 14:47):

You can access it with tactic.when_tracing `eliminate_hyp

Jannis Limperg (Jul 20 2020 at 14:49):

Awesome, thank you!

Scott Morrison (Jul 21 2020 at 01:27):

There's also trace_if_enabled `eliminate_hyp "message".


Last updated: Dec 20 2023 at 11:08 UTC