Notation for Indexed Collections

This file defines notation:

• x[i,j,k] for getting elements
• x[i,j,k] := xi for setting elements

def LeanColls.Indexed.Notation.elemIndex : Lean.ParserDescr

Element index can either be an index or a range.

Equations

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

def LeanColls.Indexed.Notation.indexedGet : Lean.TrailingParserDescr

The syntax x[i,j,k] gets the element of x : X indexed by (i,j,k). It is required that there is an instance Indexed X I E and (i,j,k) has type I.

This notation also support ranges, x[:i,j₁:j₂,k] returns a slice of x.

Note that product is right associated thus x[i,j,k], x[i,(j,k)] and x[(i,j,k)] result in the same expression.

Equations

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

def LeanColls.Indexed.Notation.«doElem__[_,,]:=_» : Lean.ParserDescr

Equations

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

def LeanColls.Indexed.Notation.«doElem__[_,,]←_» : Lean.ParserDescr

Equations

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

def LeanColls.Indexed.Notation.«doElem__[_,,]+=_» : Lean.ParserDescr

Equations

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

def LeanColls.Indexed.Notation.«doElem__[_,,]-=_» : Lean.ParserDescr

Equations

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

def LeanColls.Indexed.Notation.«doElem__[_,,]*=_» : Lean.ParserDescr

Equations

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

def LeanColls.Indexed.Notation.«doElem__[_,,]/=_» : Lean.ParserDescr

Equations

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

def LeanColls.Indexed.Notation.«doElem__[_,,]•=_» : Lean.ParserDescr

Equations

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

def LeanColls.Indexed.Notation.unexpandIndexedGet : Lean.PrettyPrinter.Unexpander

Equations

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