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

Equations

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

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.

Equations

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

def Finsupp.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 Finsupp.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 Finsupp.instReprFinsupp {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] [Zero β] : Repr (α →₀ β)

Display Finsupp using fun₀ notation.

Equations

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