toProjectionData

Mathlib.Tactic.Simps.Basic

URI: https://scilib.ai/kg/mathlib#Simps.ParsedProjectionData.toProjectionData

Lean4

/-- Turn `ParsedProjectionData` into `ProjectionData`. -/
def toProjectionData (p : ParsedProjectionData) : ProjectionData :=
  { p with name := p.newName, expr := p.expr?.getD default, projNrs := p.projNrs.toList }

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

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

Разделы

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

Аффилиация

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