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.

source
def DFinsupp.elabSingle₀ :
Lean.Elab.Term.TermElab

DFinsupp elaborator for single₀.

Equations
    Instances For
      source
      def DFinsupp.elabUpdate₀ :
      Lean.Elab.Term.TermElab

      DFinsupp elaborator for update₀.

      Equations
        Instances For
          source
          def DFinsupp.singleUnexpander :
          Lean.PrettyPrinter.Unexpander

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

          Equations
            Instances For
              source
              def DFinsupp.updateUnexpander :
              Lean.PrettyPrinter.Unexpander

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

              Equations
                Instances For
                  source
                  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.

                  Equations