Zulip Chat Archive
Stream: general
Topic: set_option to default
Reid Barton (Aug 13 2020 at 17:17):
Is there a way to set an option to its default value, whatever that is?
Scott Morrison (Aug 13 2020 at 22:55):
I think src#tactic.apply_opt_param is as close as you're going to get.
Reid Barton (Aug 13 2020 at 23:04):
Not a structure field, an option as in set_option
Last updated: May 02 2025 at 03:31 UTC