## 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 14 2021 at 13:24 UTC