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

A variant of Lean.Parser.Term.matchAlts with less line wrapping.

Equations

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

def Finsupp.fun₀ : Lean.Parser.Parser

Finsupp α M, denoted α →₀ M, is the type of functions f : α → M such that f x = 0 for all but finitely many x.

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.