From @joaopizani on March 28, 2015 18:30
Victor Miraldo has a nice-looking reflection-based library for guessing congruences and making equational-reasoning based proofs a bit less tedious (https://github.com/VictorCMiraldo/agda-rw).
We could try to instantiate and use this approach with our idea of congruence for the circuit behavioural equality (_≋_).
Copied from original issue: joaopizani/piware#38
From @joaopizani on March 28, 2015 18:30
Victor Miraldo has a nice-looking reflection-based library for guessing congruences and making equational-reasoning based proofs a bit less tedious (https://github.com/VictorCMiraldo/agda-rw).
We could try to instantiate and use this approach with our idea of congruence for the circuit behavioural equality (
_≋_).Copied from original issue: joaopizani/piware#38