{"push_id":567886805,"size":27,"distinct_size":27,"ref":"refs/heads/master","head":"b80fcfcad6c7351d5d9fb5ef399523dcb9bbe2d6","before":"934b6d213b726368aa30912b54a4d9c401e685fa","commits":[{"sha":"2e626b29fbb077d31db5b44c96239f2c8bffc2c8","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/2e626b29fbb077d31db5b44c96239f2c8bffc2c8"},{"sha":"1043cc8b48a01e1e82f22f74cf7f185109289864","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/normalize): add templates for serializing optional types","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/1043cc8b48a01e1e82f22f74cf7f185109289864"},{"sha":"39446a7215c1dda102e0393276afec060c121829","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"refactor(library/projection): move is_constructor_app to util","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/39446a7215c1dda102e0393276afec060c121829"},{"sha":"1bd1f94542c524015919460d6f38e6f1773b8752","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/normalize): add \"unfold-c\" hint to normalizer\n\nThis hint will also be used in the simplifier","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/1bd1f94542c524015919460d6f38e6f1773b8752"},{"sha":"7205382f8c179ca1818d05f0d28a4df97ac51508","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/definitional/projection): add \"unfold-c\" hint to projections","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/7205382f8c179ca1818d05f0d28a4df97ac51508"},{"sha":"ba641d7c587453cbd65e720ee43ab1ffcbde4e05","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/normalize): validate unfold-c hints","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/ba641d7c587453cbd65e720ee43ab1ffcbde4e05"},{"sha":"bc95f09828313007792c1fbc3545573fbac99b57","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean/decl_cmds): allow user to specify unfold-c hint","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/bc95f09828313007792c1fbc3545573fbac99b57"},{"sha":"979d6494e9cb3661b619151a57b709be60a2d613","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(emacs/lean-syntax): add syntax-highlight for unfold-c hint attribute","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/979d6494e9cb3661b619151a57b709be60a2d613"},{"sha":"78bde6c9e6844e6fa117553fc57fa6d6a7985be0","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"test(tests/lean/run): add more rewrite tactic tests","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/78bde6c9e6844e6fa117553fc57fa6d6a7985be0"},{"sha":"ba9557bb948fca0200d43e4e525f857d68eb291b","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(library/tactic/rewrite_tactic): incorrect assertion","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/ba9557bb948fca0200d43e4e525f857d68eb291b"},{"sha":"62daf73dd03a46be7b4772abd3424646f39f08fb","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(library/normalize): fix style","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/62daf73dd03a46be7b4772abd3424646f39f08fb"},{"sha":"b4139627e5e2418477e92ef28ab7a9dd02ed7a2f","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/tactic/rewrite_tactic): add option to prevent any kind of constant unfolding when perfoming pattern matching in the rewrite tactic","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/b4139627e5e2418477e92ef28ab7a9dd02ed7a2f"},{"sha":"5b2a9dacc25cb7a72d71145157481134fdea211b","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(library/tactic/rewrite_tactic): matcher should unfold only reducible constants","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/5b2a9dacc25cb7a72d71145157481134fdea211b"},{"sha":"7aac9f1fdbb36bf9a5966dbcedd20e10e701e7e7","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/tactic/rewrite_tactic): use expensive convertability checker at reduce_to steps and trivial goal","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/7aac9f1fdbb36bf9a5966dbcedd20e10e701e7e7"},{"sha":"5b25da8c43e39989d3ea5e735743634087db0a07","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean): add esimp tactic based on rewrite tactic\n\ncloses #358","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/5b25da8c43e39989d3ea5e735743634087db0a07"},{"sha":"04f8278c904b8162817c9ac3f7fec1b22e6e9f7c","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"test(tests/lean/run): add rewrite tactic test","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/04f8278c904b8162817c9ac3f7fec1b22e6e9f7c"},{"sha":"47bd5e53e2e2630364cce105a83d180c2284c0c2","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(library/tactic/rewrite_tactic): memory leak","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/47bd5e53e2e2630364cce105a83d180c2284c0c2"},{"sha":"aa70334f8d71a58020e1f57b9272677d97e69da2","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/tactic/rewrite_tactic): add \"fold\" step","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/aa70334f8d71a58020e1f57b9272677d97e69da2"},{"sha":"1e8a975daa193b95d1d66dcb6d9b4570ab2c5315","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean): extend parser: rewrite \"fold\" step","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/1e8a975daa193b95d1d66dcb6d9b4570ab2c5315"},{"sha":"f10424d7295c880c1bc1a99182566e4b9a6880b0","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(library/tactic/rewrite_tactic): memory leak","distinct":true,"url":"https://api.github.com/repos/soonhokong/lean-osx/commits/f10424d7295c880c1bc1a99182566e4b9a6880b0"}]}