Options API

Stream: lean4

[Marcus Rossel]

I'm confused about the API surrounding Options. If I define something like the following, what is the correct function to use in getTest such that it returns true by default and returns <x> if set_option test <x> was called?

import Lean
open Lean

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

def getTest : MetaM Bool := do
  let some result := ??? | throwError "Option not found"
  return result

[Jannis Limperg]

def getTest : MetaM Bool :=
  return test.get (← getOptions)