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.

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

DFinsupp elaborator for single₀.

Equations

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

def DFinsupp.elabUpdate₀ : Lean.Elab.Term.TermElab

DFinsupp elaborator for update₀.

Equations

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

def DFinsupp.singleUnexpander : Lean.PrettyPrinter.Unexpander

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

Equations

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

def DFinsupp.updateUnexpander : Lean.PrettyPrinter.Unexpander

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

Equations

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

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.