Finite domains for coloured cubes

@[reducible, inline]

abbrev MacMahon.Label : Type

Conway tableau labels, distinct from the six face colours.

Equations

• MacMahon.Label = Fin 6

@[reducible, inline]

abbrev MacMahon.Pair : Type

Ordered coordinates in Conway's tableau; diagonal entries are reserved.

Equations

• MacMahon.Pair = (MacMahon.Label × MacMahon.Label)

@[reducible, inline]

abbrev MacMahon.Corner : Type

The forty oriented corner types formed from the six distinct face colours.

Equations

• MacMahon.Corner = Fin 40

@[reducible, inline]

abbrev MacMahon.Slot : Type

The eight positions in a two-by-two-by-two assembly.

Equations

• MacMahon.Slot = Fin 8

@[reducible, inline]

abbrev MacMahon.Inventory : Type

Natural-number multiplicities of the tableau entries.

Equations

• MacMahon.Inventory = (MacMahon.Pair → ℕ)