{"push_id":684804008,"size":11,"distinct_size":11,"ref":"refs/heads/residuation-preserves-concurrency","head":"fc7374c3bf882fc252234130e88f21dad97db401","before":"8c4f442b801e30ac4946210aa41d7f3aad58a125","commits":[{"sha":"582ae24941f476d8fe69da2286b5632e6e4c7d4b","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"Hmm, don't think I need the 'with' clauses for 'pop' etc at all...","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/582ae24941f476d8fe69da2286b5632e6e4c7d4b"},{"sha":"33b37c79d339176418dfe82a3379e4d4eaabd57f","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"Current ratio is a factor 5 increase in proof size.","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/33b37c79d339176418dfe82a3379e4d4eaabd57f"},{"sha":"b3ce3a1047e036995a2b234c8612866b78f55063","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"Losing some of the remaining 'with' clauses will help slightly...","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/b3ce3a1047e036995a2b234c8612866b78f55063"},{"sha":"03d19271f8f3581c5dfab1fe2bee7dd59bd0ebdb","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"6 requirements for that lemma so far...","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/03d19271f8f3581c5dfab1fe2bee7dd59bd0ebdb"},{"sha":"3942a920420f7119f5abbf0e026f426c12e3e3b0","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"As a precursor to the lemma, introduce a specialised version of the current theorem.","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/3942a920420f7119f5abbf0e026f426c12e3e3b0"},{"sha":"7fe3b35964d1475fd6b1f4d14db9709023e5da04","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"Extract required behaviour into specialised theorem.","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/7fe3b35964d1475fd6b1f4d14db9709023e5da04"},{"sha":"c6fb12a54bcd367942ef53d6a32c884033a4d936","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"Extract required behaviour into specialised theorem.","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/c6fb12a54bcd367942ef53d6a32c884033a4d936"},{"sha":"03a9cbe23b15d03fcab141712022f57f2cabd453","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"Ah, the reason I don't need the pop-related 'with's any more is that the definition of 'residual' no longer uses them.","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/03a9cbe23b15d03fcab141712022f57f2cabd453"},{"sha":"8fd201c24c9cebe00afbc7834799712232a23aac","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"Some progress on this first case, but still tricky.","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/8fd201c24c9cebe00afbc7834799712232a23aac"},{"sha":"265b04711b139e9f990457ac09dc441d69f6243c","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"8 sub-cases left of case 1 of 29 cases.","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/265b04711b139e9f990457ac09dc441d69f6243c"},{"sha":"fc7374c3bf882fc252234130e88f21dad97db401","author":{"email":"fbb2ede0988223be61002b98c39c313addc1ce7f@dynamicaspects.org","name":"Roly Perera"},"message":"Some refinement of goals, but still slow progress.","distinct":true,"url":"https://api.github.com/repos/rolyp/proof-relevant-pi/commits/fc7374c3bf882fc252234130e88f21dad97db401"}]}