getStacksTag

Mathlib.Tactic.StacksAttribute

URI: https://scilib.ai/kg/mathlib#Lean.TSyntax.getStacksTag

Lean4

/-- Extract the underlying tag as a string from a `stacksTag` node. -/
def getStacksTag (stx : TSyntax stacksTagKind) : CoreM String := do
  let some val := Syntax.isLit? stacksTagKind stx |
    throwError"Malformed Stacks tag"
  return val

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

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

Разделы

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

Аффилиация

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