Documentation

Mathlib.Data.DFinsupp.Notation

Notation for DFinsupp #

This file extends the existing fun₀ | 3 => a | 7 => b notation to work for DFinsupp, which desugars to DFinsupp.update and DFinsupp.single, in the same way that {a, b} desugars to insert and singleton.

Note that this syntax is for Finsupp by default, but works for DFinsupp if the expected type is correct.

DFinsupp elaborator for single₀.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    DFinsupp elaborator for update₀.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Unexpander for the fun₀ | i => x notation.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Unexpander for the fun₀ | i => x notation.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          unsafe instance DFinsupp.instRepr {α : Type u_1} {β : αType u_2} [Repr α] [(i : α) → Repr (β i)] [(i : α) → Zero (β i)] :
          Repr (Π₀ (a : α), β a)

          Display DFinsupp using fun₀ notation.