elabUnsetOption

Mathlib.Tactic.UnsetOption

URI: https://scilib.ai/kg/mathlib#Lean.Elab.elabUnsetOption

Lean4

/-- unset the option specified by id -/
def elabUnsetOption (id : Syntax) : m Options := do
  -- We include the first argument (the keyword) for position information in case `id` is `missing`.

  addCompletionInfo <| CompletionInfo.option (← getRef)
  unsetOption id.getId.eraseMacroScopes
where/-- unset the given option name -/
   unsetOption (optionName : Name) : m Options := return (← getOptions).erase optionName

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru