{"push_id":935086435,"size":23,"distinct_size":23,"ref":"refs/heads/master","head":"f2eef7aa1b7c9b7ed8a3147acb62567263dc789a","before":"f7494618ff231447f87860d3024358bf1cab30b5","commits":[{"sha":"8f7b533ca1c38484b893c9af9883057f3f176527","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"refactor(library): move 'cast' to init folder","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/8f7b533ca1c38484b893c9af9883057f3f176527"},{"sha":"3643e79cb366a686194aa7e08b72a1ea8307f46b","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/blast/congruence_closure): improve the suppoer for subsingletons in the ematching procedure","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/3643e79cb366a686194aa7e08b72a1ea8307f46b"},{"sha":"8fded5224b7fb97dbf0a51e541b15d51ab3f8111","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(library/blast/congruence_closure): improve comment","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/8fded5224b7fb97dbf0a51e541b15d51ab3f8111"},{"sha":"723a9e227a3ed267a260f094dbf81316ca7349ba","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(kernel/default_converter): remove dead code","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/723a9e227a3ed267a260f094dbf81316ca7349ba"},{"sha":"c19be9d9e71732094b800590d8cc2308505f2a78","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/util): add is_app_of helper function","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/c19be9d9e71732094b800590d8cc2308505f2a78"},{"sha":"b975717875d92490ce6cdc6d02dafe10263bd0d4","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(init/logic): add cast_heq","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/b975717875d92490ce6cdc6d02dafe10263bd0d4"},{"sha":"599ec08c701eccd337dcb687a3ddac7e0e272173","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/blast/congruence_closure): add support for eq.rec and cast in the congruence closure module","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/599ec08c701eccd337dcb687a3ddac7e0e272173"},{"sha":"58d41e486ca11b7cdf4020f27172c8d68b0530ff","author":{"email":"05c7c2712eab81287658c607466a3eb2b59dcd80@gmail.com","name":"Daniel Selsam"},"message":"feat(library/trace): register debug trace class","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/58d41e486ca11b7cdf4020f27172c8d68b0530ff"},{"sha":"ba16d188e61b832376fa39c4b314885057270a28","author":{"email":"05c7c2712eab81287658c607466a3eb2b59dcd80@gmail.com","name":"Daniel Selsam"},"message":"feat(library/blast/forward/ematch): basic debug tracing","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/ba16d188e61b832376fa39c4b314885057270a28"},{"sha":"b1d32bbaf639c9a7a0759c298481b6c5a8a3ef88","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(library/blast/forward/ematch): more tracing","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/b1d32bbaf639c9a7a0759c298481b6c5a8a3ef88"},{"sha":"05c3ede683b3811c165b148f491b7fd729902ad8","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(tests/lean/run/blast_vector_test): test ematch + cc at vectors","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/05c3ede683b3811c165b148f491b7fd729902ad8"},{"sha":"912c5254def32faa550079f03e2574e8fcb6faa8","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(tests/lean/run/cases_bug): adjust test to changes in the std lib","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/912c5254def32faa550079f03e2574e8fcb6faa8"},{"sha":"1048812e2eb262b711d576eda8102486bd2526c2","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(frontends/lean/notation_cmd): cleanup weird coding pattern","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/1048812e2eb262b711d576eda8102486bd2526c2"},{"sha":"f0cc98ebb5b134b7738f66b3e726bba217134dc1","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(library/blast/recursor/recursor_action): disable spurious warning","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/f0cc98ebb5b134b7738f66b3e726bba217134dc1"},{"sha":"d9294fc1647837d23f2c5ce30a8f9ac129729123","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(kernel/expr): remove dead var","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/d9294fc1647837d23f2c5ce30a8f9ac129729123"},{"sha":"3f7122ce074751222b9767a30ab26395bec0dc16","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/blast/congruence_closure): more general congruence lemmas","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/3f7122ce074751222b9767a30ab26395bec0dc16"},{"sha":"8d49e42ec26bfd0a1e840bdf9f82c4d482b29eeb","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(library/blast/congruence_closure): user-defined congruence lemmas for equality and relation congruences","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/8d49e42ec26bfd0a1e840bdf9f82c4d482b29eeb"},{"sha":"7a005fb76ba48dff165c112be034c5ec257776f0","author":{"email":"05c7c2712eab81287658c607466a3eb2b59dcd80@gmail.com","name":"Daniel Selsam"},"message":"test(tests/lean/run/blast_vector_test): more tests","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/7a005fb76ba48dff165c112be034c5ec257776f0"},{"sha":"abbffc74360284f80f9e22fbee06feaa89c91c75","author":{"email":"05c7c2712eab81287658c607466a3eb2b59dcd80@gmail.com","name":"Daniel Selsam"},"message":"feat(library/blast/forward/ematch): more tracing","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/abbffc74360284f80f9e22fbee06feaa89c91c75"},{"sha":"37fdac4d652bc84c7903fe9a651821d9427cc32d","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"test(tests/lean/run/blast_cc_heq9): add new test","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean/commits/37fdac4d652bc84c7903fe9a651821d9427cc32d"}]}