From @joaopizani on March 28, 2015 18:25
We had to develop a lot of "indexed" things for expressing circuit equality "up to simulation", due to the fact that we were dealing with an equality over an indexed datatype in which the two sides of the equality could (possibly) have different indices.
Now we have basically a mirror of Agda's stdlib modules Relation.Binary{,.Core}, etc. with the "Indexed" suffix. We should submit this upstream.
Copied from original issue: joaopizani/piware#34
From @joaopizani on March 28, 2015 18:25
We had to develop a lot of "indexed" things for expressing circuit equality "up to simulation", due to the fact that we were dealing with an equality over an indexed datatype in which the two sides of the equality could (possibly) have different indices.
Now we have basically a mirror of Agda's stdlib modules Relation.Binary{,.Core}, etc. with the "Indexed" suffix. We should submit this upstream.
Copied from original issue: joaopizani/piware#34