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