getVarsToClear

Mathlib.Tactic.ClearExcept

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

Lean4

/-- Returns the free variable IDs that can be cleared, excluding those in the preserve list
and class instances. -/
def getVarsToClear (preserve : Array FVarId) : MetaM (Array FVarId) := do
  let mut toClear : Array FVarId := #[]
  for decl in ← getLCtx do
    unless preserve.contains decl.fvarId do
      if let none← isClass? decl.type then
        toClear := toClear.push decl.fvarId
  return toClear

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

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

Разделы

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

Аффилиация

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