cleanBinders

Mathlib.Tactic.Variable

URI: https://scilib.ai/kg/mathlib#Mathlib.Command.Variable.cleanBinders

Lean4

/-- Strip off whitespace and comments. -/
def cleanBinders (binders : TSyntaxArray ``bracketedBinder) : TSyntaxArray ``bracketedBinder :=
  Id.run
    (do
      let mut binders' := #[]
      for binder in binders do
        binders' := binders'.push <| ⟨binder.raw.unsetTrailing⟩
      return binders')

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

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

Разделы

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

Аффилиация

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