Documentation

Complexity.Computability.PCP.Encoded.AssignmentTester.Enumeration

Constructive enumeration of assignment-tester coins #

The conjunction and selected testers use the same product coins. Batching their component enumerations keeps instance synthesis within its ordinary limits.

Main definitions #

References #

source
@[instance_reducible]
def Cslib.PCP.HadamardTester.instFinEnumBool :
FinEnum Bool

Concrete bit enumeration, registered locally while constructing the tester's coins.

Instances For
    source
    @[instance_reducible]
    def Cslib.PCP.HadamardTester.Rand.finEnum (α : Type) [FinEnum α] :
    FinEnum (Rand α)

    Constructively enumerate the tester's coins. Batching the repeated factors keeps the nested product within instance-synthesis limits.

    Instances For