whatsNew

Mathlib.Util.WhatsNew

URI: https://scilib.ai/kg/mathlib#Mathlib.WhatsNew.whatsNew

Lean4

def whatsNew (old new : Environment) : CoreM MessageData := do
  let mut diffs := #[]
  for (c, i) in new.constants.map₂.toList do
    unless old.constants.map₂.contains c do
      diffs := diffs.push (← printIdCore c i)
  for ext in ← persistentEnvExtensionsRef.get do
    if let some diff := ← diffExtension old new ext then
      diffs := diffs.push diff
  if diffs.isEmpty then
    return "no new constants"
  pure <| MessageData.joinSep diffs.toList "\n\n"

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

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

Разделы

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

Аффилиация

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