Reading options with default values

Stream: lean4

[Eric Wieser]

What's the right way to read a boolean option? I was able to get

import Std

open Lean

register_option myOption : Bool :=
  { defValue := true }

#eval show MetaM _ from do
  getBoolOption myOption.name (← getOptionDefaultValue myOption.name).getBoolEx

to work, but surely there is some API somewhere that respects the option default value?

[Alex J. Best]

myOption.get

[Eric Wieser]

Thanks!