{"push_id":2706054903,"size":3,"distinct_size":3,"ref":"refs/heads/master","head":"792e41c159eed1b7ebba6a520b6a069fbe840ee5","before":"d5018c66863cab07866ddb84dc25503edb81b1b2","commits":[{"sha":"eff0eb428555e88027f0196eccf29f36fb0aa9e7","author":{"name":"Joachim Breitner","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@joachim-breitner.de"},"message":"Move `extendInScopeSetList` realated lemmas to `VarSet.v`","distinct":true,"url":"https://api.github.com/repos/antalsz/hs-to-coq/commits/eff0eb428555e88027f0196eccf29f36fb0aa9e7"},{"sha":"b0a4236ca8118dab230147c0c1d6caacf14adbec","author":{"name":"Joachim Breitner","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@joachim-breitner.de"},"message":"More moving lemmas to right module","distinct":true,"url":"https://api.github.com/repos/antalsz/hs-to-coq/commits/b0a4236ca8118dab230147c0c1d6caacf14adbec"},{"sha":"792e41c159eed1b7ebba6a520b6a069fbe840ee5","author":{"name":"Joachim Breitner","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@joachim-breitner.de"},"message":"Exitify done! 🎆\n\nHere is the main theorem:\n\n    Theorem exitifyProgram_WellScoped_JPV:\n      forall pgm,\n      WellScopedProgram pgm ->\n      isJoinPointsValidProgram pgm ->\n      WellScopedProgram (exitifyProgram pgm) /\\\n      isJoinPointsValidProgram (exitifyProgram pgm).\n\nOf course, the are plenty of Admitted things in modules that this\ndepends on, e.g. JoinPointInvariants.v, VarSet.v, ScopeInvariant.v. But\nall the stuff that relates to Exitification is proven.","distinct":true,"url":"https://api.github.com/repos/antalsz/hs-to-coq/commits/792e41c159eed1b7ebba6a520b6a069fbe840ee5"}]}
{"actor":{"display_login":"nomeata"}}