Small examples

These definitions give named vertices and distributions for testing the basic API on low-dimensional cubes.

def PebblingLean.Hypercube.zeroVertex (n : ℕ) : HypercubeVertex n

The all-zero vertex of a hypercube.

Equations

• PebblingLean.Hypercube.zeroVertex n x✝ = false

def PebblingLean.Hypercube.oneVertex (n : ℕ) : HypercubeVertex n

The all-one vertex of a hypercube.

Equations

• PebblingLean.Hypercube.oneVertex n x✝ = true

theorem PebblingLean.Hypercube.dist_zero_zero (n : ℕ) : dist (zeroVertex n) (zeroVertex n) = 0

def PebblingLean.Examples.squareThreeAtZero : Pebbling (HypercubeVertex 2)

Three pebbles on one vertex of the square Q_2.

Equations

• PebblingLean.Examples.squareThreeAtZero x = if x = PebblingLean.Hypercube.zeroVertex 2 then 3 else 0