Zulip Chat Archive

Stream: lean4

Topic: set_option list

Jason Gross (Mar 12 2021 at 19:55):

Is there a way to query lean for all the options I can set with set_option?

Bryan Gin-ge Chen (Mar 12 2021 at 20:13):

I haven't tested this out recently, but I wrote a snippet to list the options here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.23help/near/221643103

Jason Gross (Mar 12 2021 at 20:14):

Thanks!

Jason Gross (Mar 12 2021 at 20:15):

Unfortunately I get unknown identifier 'Lean.OptionDecl' and unknown identifier 'Lean.getOptionDeclsArray'

Bryan Gin-ge Chen (Mar 12 2021 at 20:18):

Ah, sorry. I forgot to put import Lean at the top of my snippet. (Just edited it in.)

Last updated: Dec 20 2023 at 11:08 UTC