{"push_id":2727998081,"size":9,"distinct_size":9,"ref":"refs/heads/proof-dev","head":"b21b49269e54465918b88f4ae54f6682c1d21b19","before":"16165a0dcbc8748b90e4afbc233356f9d9faa097","commits":[{"sha":"cbe9c6ccc0887af0de25a0d54895ad8fd6c5fc6e","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: change the condition on u_t_sum\n\nadditionally, update uval_typing_bang","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/cbe9c6ccc0887af0de25a0d54895ad8fd6c5fc6e"},{"sha":"fa6a623c09089da4ac3a0fac9fea8ef95d9c8db1","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: fix the u_sem_promote case","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/fa6a623c09089da4ac3a0fac9fea8ef95d9c8db1"},{"sha":"d668276380945f509b769071f96ef9580ffa520b","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: fix u_sem_con case\n\nMost importantly, the update semantics for sums now only hold the\ncases still to be discharged by case analysis.","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/d668276380945f509b769071f96ef9580ffa520b"},{"sha":"823cb13791c8a663fed1834bae44a0d916139b2c","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: correctly map tags on USum\n\nWe only want to consider the variants that are not taken.","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/823cb13791c8a663fed1834bae44a0d916139b2c"},{"sha":"75eecf3a56bf616152a6cd749a8a396a3739f314","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: rewrite sum_downcast_u","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/75eecf3a56bf616152a6cd749a8a396a3739f314"},{"sha":"5f4c7c7296910038cd3af5dc7b5da04944037d90","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: complete case u_sem_esac for preservation","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/5f4c7c7296910038cd3af5dc7b5da04944037d90"},{"sha":"69fb74ba814acb2321fa213ab14a6387dd03d7f5","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: remove unnecessary arbitrary k","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/69fb74ba814acb2321fa213ab14a6387dd03d7f5"},{"sha":"0f37e42d63dcee9e9097e0c5622abea6c0bb10ee","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: fix u_sem_con case in preservation\n\nUpdates the u_sem_con case to be in line with the new semantics.\n\nNotably, filters the initial tags on the USum side so we only store the tag that's being constructed.","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/0f37e42d63dcee9e9097e0c5622abea6c0bb10ee"},{"sha":"b21b49269e54465918b88f4ae54f6682c1d21b19","author":{"name":"vjackson725","email":"2933212c3996690341c5bf59ddd5cfae014c23a3@users.noreply.github.com"},"message":"proof: update uval_typing_bang","distinct":true,"url":"https://api.github.com/repos/vjackson725/cogent/commits/b21b49269e54465918b88f4ae54f6682c1d21b19"}]}
{"actor":{"display_login":"vjackson725"}}