Test value of option

Stream: lean4

[Bhavik Mehta]

I presume this is a simple question, but I couldn't find the answer anywhere. How can I test the value of an option? That is, what command can I run to get lean to tell me whether autoImplicit is turned on in my file or not?

[Bhavik Mehta]

I found

#eval Lean.getOptionDecl `autoImplicit

but this only tells me the default value, not the current value. Presumably I need to pass in the current env to the correct function, or the IO monad is handling that

[Bhavik Mehta]

Ah! Found it:

#eval Lean.getBoolOption `autoImplicit

[Jannis Limperg]

For a more type-safe alternative, you can also use Lean.Elab.autoImplicit.get. Here docs#Lean.Elab.autoImplicit is a docs#Lean.Option; one of these is automatically created when an option is registered.

[Bhavik Mehta]

Ah, so then I can say

#eval Lean.Elab.autoImplicit.get <$> Lean.getOptions

and the idea is that now if I misspell the option name, I get an error rather than a junk value?

[Jannis Limperg]

Yes, exactly! And you also get a type error if you try to get a Nat out of a Bool-valued Lean.Option.

[Bhavik Mehta]

Amazing, thank you!