Circuit and Plugs modules with size-only indices
went further with the Synthesizable "typeclass" in Circuit.agda
Synthesizable Vec "instance", sketching eval
after meeting, FIXED Circ into datatype for eval, indices unifying
on the way to defining high-level Plugs.agda
high-level plugs done, using a postulate that relates >= and <=
forking plugs
most samples working in "high-level", organized Circuit.agda a bit
cleaned-up imports, aggregated instances
Intertwine plug
using algebraic structure (monoid) in proofs of plugs
began to split in modules
split into modules, issues: exploding number of instances, parameterize on atom
trying to clean up arguments of instances and plugs as much as possible
made pair destructor plugs, refactored Core plugs shorter
finished converting samples, one postulate (needed for rippleCarry) left
done proof samples, except ripple-carry, will merge with master