|
|
|---|
|
|
|
|---|
Indexed names for PFCS families.
Some PFCS gadgets are actually parameterized families, with varying numbers of variables and/or constraints. In order to formalize these gadgets, we need to generate names (of relations and variables) that are parameterized, generally over numbers.
To this end, this file introduces a notion of indexed names, i.e. names consisting of a base (a prefix) and a numeric index, separated from the base with an underscore.
We introduce constructors for these indexed names, and we prove properties of them, useful in proofs about parameterized gadgets.
All of this is really more general than PFCS, so it could be moved to a more central place at some point.