instToExprOfToLevel

Mathlib.Data.Multiset.Sort

URI: https://scilib.ai/kg/mathlib#Multiset.instToExprOfToLevel

Lean4

unsafe instance {α : Type u} [Lean.ToLevel.{u}] [Lean.ToExpr α] : Lean.ToExpr (Multiset α) :=
  haveI u' := Lean.toLevel.{u}
  haveI α' : Q(Type u') := Lean.toTypeExpr α
  { toTypeExpr := q(Multiset $α')
    toExpr
      s :=
      show Q(Multiset $α') from
        if Multiset.card s = 0 then q(0) else mkSetLiteralQ (α := q($α')) q(Multiset $α') (s.unquot.map Lean.toExpr) }
    -- TODO: use a sort order if available, gh-18166

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

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

Разделы

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

Аффилиация

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