hazelgrove/agda-popl17

coherence between heads of the two branches

Closed this issue · 1 comments

make sure that the right back propagation and such happens so that the sums branch is strictly additive on to the master.

Did this manually this afternoon. The only weird stuff now relates to the alternative form of determinism, because I'm working on it in the smaller fragment, and that's OK. Need to avoid this nonsense in the future by learning more about git.