def Lean.Elab.elabSetOption {m : Type → Type} [Monad m] [Lean.MonadOptions m] [MonadExceptOf Lean.Exception m] [Lean.MonadRef m] [Lean.AddErrorMessageContext m] [MonadLiftT (EIO Lean.Exception) m] [Lean.Elab.MonadInfoTree m] (id val : Lean.Syntax) : m Lean.Options

def Lean.Elab.elabSetOption.setOption {m : Type → Type} [Monad m] [Lean.MonadOptions m] [MonadExceptOf Lean.Exception m] [Lean.MonadRef m] [Lean.AddErrorMessageContext m] (optionName : Lean.Name) (decl : Lean.OptionDecl) (val : Lean.DataValue) : m Lean.Options