declAbstractNestedProofs

Mathlib.Tactic.ToAdditive.Frontend

URI: https://scilib.ai/kg/mathlib#ToAdditive.declAbstractNestedProofs

Lean4

/-- Abstracts the nested proofs in the value of `decl` if it is a def. -/
def declAbstractNestedProofs (decl : ConstantInfo) : MetaM ConstantInfo := do
  if decl matches .defnInfo _ then
    return
      decl.updateValue <|
        ←
          withDeclNameForAuxNaming decl.name do
            Meta.abstractNestedProofs decl.value!
  else
    return decl

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

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

Разделы

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

Аффилиация

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