instRepr

Mathlib.Data.Finsupp.Notation

URI: https://scilib.ai/kg/mathlib#Finsupp.instRepr

Lean4

/-- Display `Finsupp` using `fun₀` notation. -/
unsafe instance instRepr {α β} [Repr α] [Repr β] [Zero β] : Repr (α →₀ β) where
  reprPrec f
    p :=
    if f.support.card = 0 then "0"
    else
      let ret : Std.Format :=
        f!"fun₀" ++
          .nest 2
            (.group
              (.join <|
                f.support.val.unquot.map fun a => .line ++ .group ((f! "| {repr a} =>") ++ .line ++ repr (f a))))
      if p ≥ leadPrec then Format.paren ret else ret

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

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

Разделы

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

Аффилиация

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