set-option option docs?

Stream: new members

[Ada Weird]

Hello, I was wondering if there was one centralized place I could go to look at any of the options I can use with set_option. Also some way to push the current set of options on the stack, set the options I need, do whatever, and then pop back to the options before I meddled with them would be much appreciated.

[Michael Rothgang]

A set_option only takes effect for the current section or namespace --- so you should be able to put your code with different options in a section.

[Michael Rothgang]

For your first question, there's #help option: this will tell you about the options you can use that this point.

[Ada Weird]

Ah okay. Yeah that works for me.

[Ada Weird]

Thank you!

[Michael Rothgang]

(Lean code can define new option, so "one place to list all options there are" cannot quite exist.)

[Ada Weird]

Ah I see. I'm just learning so I didn't know about that.

[Michael Rothgang]

No worries! I just learned about #help option myself :-)

[Michael Rothgang]

#help also has a few other variants, which are occasionally helpful.

[Michael Rothgang]

To get a list of all mathlib tactics that is nicer to read and curated, I prefer this over #help tactic, though.