expandLemma

Mathlib.Tactic.Lemma

URI: https://scilib.ai/kg/mathlib#expandLemma

Lean4

/-- Implementation of the `lemma` command, by macro expansion to `theorem`. -/
@[macro «lemma»]
def expandLemma : Macro :=
  fun stx =>
    -- Not using a macro match, to be more resilient against changes to `lemma`.
      -- This implementation ensures that any future changes to `theorem` are reflected in `lemma`

  let stx :=
    stx.modifyArg 1 fun stx =>
      let stx := stx.modifyArg 0 (mkAtomFrom · "theorem" (canonical := true))
      stx.setKind ``Parser.Command.theorem
  pure <| stx.setKind ``Parser.Command.declaration

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

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

Разделы

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

Аффилиация

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