instToExprPUnitOfToLevel_mathlib

Mathlib.Tactic.ToExpr

URI: https://scilib.ai/kg/mathlib#Mathlib.instToExprPUnitOfToLevel_mathlib

Lean4

/-- Hand-written instance since `PUnit` is a `Sort` rather than a `Type`. -/
instance [ToLevel.{u}] : ToExpr PUnit.{u + 1}
    where
  toExpr _ := mkConst ``PUnit.unit [toLevel.{u + 1}]
  toTypeExpr := mkConst ``PUnit [toLevel.{u + 1}]

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

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

Разделы

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

Аффилиация

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