def
Lean.Elab.elabSetOption
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadOptions m]
[inst : MonadExceptOf Lean.Exception m]
[inst : Lean.MonadRef m]
[inst : Lean.AddErrorMessageContext m]
[inst : MonadLiftT (EIO Lean.Exception) m]
[inst : Lean.Elab.MonadInfoTree m]
(id : Lean.Syntax)
(val : Lean.Syntax)
:
Equations
- Lean.Elab.elabSetOption id val = (fun setOption => do let ref ← Lean.getRef Lean.Elab.addCompletionInfo (Lean.Elab.CompletionInfo.option (Lean.Syntax.setArgs ref (Array.ofSubarray (Array.toSubarray (Lean.Syntax.getArgs ref) 0 2)))) let optionName : Lean.Name := Lean.Name.eraseMacroScopes (Lean.Syntax.getId id) match Lean.Syntax.isStrLit? val with | some str => setOption optionName (Lean.DataValue.ofString str) | none => match Lean.Syntax.isNatLit? val with | some num => setOption optionName (Lean.DataValue.ofNat num) | none => match val with | Lean.Syntax.atom x "true" => setOption optionName (Lean.DataValue.ofBool true) | Lean.Syntax.atom x "false" => setOption optionName (Lean.DataValue.ofBool false) | x => Lean.throwError (Lean.toMessageData "unexpected set_option value " ++ Lean.toMessageData val ++ Lean.toMessageData "")) Lean.Elab.elabSetOption.setOption
def
Lean.Elab.elabSetOption.setOption
{m : Type → Type}
[inst : Monad m]
[inst : Lean.MonadOptions m]
[inst : MonadExceptOf Lean.Exception m]
[inst : Lean.MonadRef m]
[inst : Lean.AddErrorMessageContext m]
[inst : MonadLiftT (EIO Lean.Exception) m]
(optionName : Lean.Name)
(val : Lean.DataValue)
:
Equations
- Lean.Elab.elabSetOption.setOption optionName val = do let ref ← Lean.getRef let decl ← liftM (IO.toEIO (fun ex => Lean.Exception.error ref (Function.comp Lean.MessageData.ofFormat Lean.format (IO.Error.toString ex))) (Lean.getOptionDecl optionName)) let _do_jp : PUnit → m Lean.Options := fun y => do let a ← Lean.getOptions pure (Lean.KVMap.insert a optionName val) if Lean.DataValue.sameCtor decl.defValue val = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "type mismatch at set_option") _do_jp y