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.Internal.elabSingle₀ :
Lean.Elab.Term.TermElab

DFinsupp elaborator for single₀.

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

    DFinsupp elaborator for update₀.

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

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

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

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

        Instances For
          source
          @[implicit_reducible]
          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.