Tests for Variables: the key of a VariableName is filled in as a literal, NameNe and disjointness of variable slots are found by instance search, and setParams writes the parameter slots.

Variable names

@[reducible, inline]

abbrev GaudisCrypt.testVarX : VariableName

Equations

• GaudisCrypt.testVarX = { name := "x", type := ℤ, nonempty := ⋯, key := 121, keyCorrect := GaudisCrypt.testVarX._proof_1 }

def GaudisCrypt.testVarY : VariableName

Equations

• GaudisCrypt.testVarY = { name := "y", type := ℤ, nonempty := ⋯, key := 122, keyCorrect := GaudisCrypt.testVarY._proof_1 }

Variable slots