{"push_id":672032956,"size":9,"distinct_size":2,"ref":"refs/heads/cubical","head":"389cf11063900a5c0ce564c0052400483516eec3","before":"4da0f07e0ec6650aa8aa6f339bd28b6e488d7e38","commits":[{"sha":"b83b0c00179c20dcef012a6d5bddf6f60c872f3f","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(library/tactic/induction_tactic): fixes #619","distinct":false,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/b83b0c00179c20dcef012a6d5bddf6f60c872f3f"},{"sha":"d47e76b2286c5b51873519d99b8a8de13495ea33","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(library.data.int.basic): move theorems about successor and predecessor from HoTT to standard library","distinct":false,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/d47e76b2286c5b51873519d99b8a8de13495ea33"},{"sha":"a789df1e254485ffed4cc46bb5c1a64c6dddd6d8","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(reserved_notation): make is_typeof parsing-only, add ^ to HoTT","distinct":false,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/a789df1e254485ffed4cc46bb5c1a64c6dddd6d8"},{"sha":"256ea9c115bde11f356001f2853c6ca7368838a4","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(hott): add recursor attribute to hits\n\nrecursor attribute is added to both the dependent and nondependent elimination, is such a way that the dependent elimination is used by default","distinct":false,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/256ea9c115bde11f356001f2853c6ca7368838a4"},{"sha":"dcfa4c04eff08ebd1d34979d8a3a2961a6b4dfff","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(hit): start using induction tactic","distinct":false,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/dcfa4c04eff08ebd1d34979d8a3a2961a6b4dfff"},{"sha":"754c2fd54fc9c60a6076938aa3ac3305081a67f6","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(lean-syntax): color abbreviations yellow","distinct":false,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/754c2fd54fc9c60a6076938aa3ac3305081a67f6"},{"sha":"59a3508bd9dbc44f2942fbd76d0c2b363e99cece","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(hott): small changes in init and category","distinct":false,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/59a3508bd9dbc44f2942fbd76d0c2b363e99cece"},{"sha":"7c9a636e1d9f2a184544cd1aa31dc60978dcb6b6","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(hott): use pathovers in all the recursors of hits\n\nmove pathover file to the standard library","distinct":true,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/7c9a636e1d9f2a184544cd1aa31dc60978dcb6b6"},{"sha":"389cf11063900a5c0ce564c0052400483516eec3","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(types): incorporate pathovers in the files of the types folder","distinct":true,"url":"https://api.github.com/repos/fpvandoorn/lean/commits/389cf11063900a5c0ce564c0052400483516eec3"}]}