Notation for Finsupp

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

def Finsupp.fun₀.matchAlts : Lean.Parser.Parser

def Finsupp.fun₀ : Lean.Parser.Parser

fun₀ | i => a is notation for Finsupp.single i a, and with multiple match arms, fun₀ ... | i => a is notation for Finsupp.update (fun₀ ...) i a.

As a result, if multiple match arms coincide, the last one takes precedence.

If the expected type is Π₀ i, α i (DFinsupp) and Mathlib/Data/DFinsupp/Notation.lean is imported, then this is notation for DFinsupp.single and Dfinsupp.update instead.

def Finsupp.Internal.stxSingle₀ : Lean.ParserDescr

Implementation detail for fun₀, used by both Finsupp and DFinsupp

def Finsupp.Internal.stxUpdate₀ : Lean.ParserDescr

Implementation detail for fun₀, used by both Finsupp and DFinsupp

def Finsupp.Internal.elabSingle₀ : Lean.Elab.Term.TermElab

Finsupp elaborator for single₀.

def Finsupp.Internal.elabUpdate₀ : Lean.Elab.Term.TermElab

Finsupp elaborator for update₀.

def Finsupp.singleUnexpander : Lean.PrettyPrinter.Unexpander

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

def Finsupp.updateUnexpander : Lean.PrettyPrinter.Unexpander

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

@[implicit_reducible]

unsafe instance Finsupp.instRepr {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] [Zero β] : Repr (α →₀ β)

Display Finsupp using fun₀ notation.