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
Last updated: May 14 2021 at 13:24 UTC