Zulip Chat Archive

Stream: lean4

Topic: set_option list


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jason Gross (Mar 12 2021 at 20:14):

Thanks!

view this post on Zulip Jason Gross (Mar 12 2021 at 20:15):

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

view this post on Zulip 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: May 18 2021 at 23:14 UTC