erase

Mathlib.Tactic.NormNum.Core

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.NormNums.erase

Lean4

/-- Erase a name marked as a `norm_num` attribute.

Check that it does in fact have the `norm_num` attribute by making sure it names a `NormNumExt`
found somewhere in the state's tree, and is not erased.
-/
def erase {m : Type → Type} [Monad m] [MonadError m] (d : NormNums) (declName : Name) : m NormNums := do
  unless d.tree.values.any (·.name == declName) && !d.erased.contains declName do
    throwError "'{declName}' does not have [norm_num] attribute"
  return d.eraseCore declName

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

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

Разделы

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

Аффилиация

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