option のデフォルト値を取得する関数

[Seasawher]

open Lean Elab Command

def getDefaultValue (opt : Name) : CommandElabM Unit := do
  let decls ← getOptionDecls
  match decls.find? opt with
  | some decl =>
    logInfo m!"default value of {opt} is {decl.defValue}"
  | none =>
    logInfo m!"{opt} is unknown"

#eval getDefaultValue `autoImplicit
#eval getDefaultValue `relaxedAutoImplicit
#eval getDefaultValue `linter.flexible

[Seasawher]

Zulip: check dafault value of option