curate diff between sum and master

Question

curate diff between sum and master

Closed this issue 8 years ago · 2 comments

Answer 1 · 2016-09-27T13:29:56.000Z

actually merging the changes to master into sums seems to make https://github.com/hazelgrove/agda-popl17/compare/sums display the thing that we want it to display. so. better discipline about that should more or less solve this problem. (unless i still don't understand the semantics of that URL.)

Answer 2 · 2016-09-27T13:45:32.000Z

also check for weird implicit arguments inconsistencies. specifically in determinism, but more generally.