{"push_id":1250433287,"size":56,"distinct_size":30,"ref":"refs/heads/inductive_compiler","head":"12cd8bf33c3572c2a77affbf050ae76bd951c8fd","before":"bf800e7a3284948aa78535720e775673c8eb3996","commits":[{"sha":"a0a72b5b82d3a1d2268a757f7e42c4b7f530edfd","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(frontends/lean): move local_context_adapter to separate folder","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/a0a72b5b82d3a1d2268a757f7e42c4b7f530edfd"},{"sha":"e5cf12e2ade5ec2f9decf33624b05b910d8e6c68","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(frontends/lean/elaborator): cleanup interface","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/e5cf12e2ade5ec2f9decf33624b05b910d8e6c68"},{"sha":"8498bbaeff42d41b52f2827fd8c1a4637eafd9b3","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(frontends/lean/elaborator): allow elaborator to add auxiliary definitions","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/8498bbaeff42d41b52f2827fd8c1a4637eafd9b3"},{"sha":"0014d9d212e43f8089b23c5c332fdb00db1a7c2a","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(emacs/lean-syntax): add 'def' and 'mutual_def'","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/0014d9d212e43f8089b23c5c332fdb00db1a7c2a"},{"sha":"ae6219ba28adc084ae859a7ec809657f83ba9c95","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(frontends/lean/elaborator): improve API","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/ae6219ba28adc084ae859a7ec809657f83ba9c95"},{"sha":"8f33269286f6c96d558db9976a34ee945e17c66d","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(frontends/lean): add decl_util module for definition/inductive commands","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/8f33269286f6c96d558db9976a34ee945e17c66d"},{"sha":"f5c35f8d762f9098f61f3dfc34bd9d60a3afd2ea","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"chore(*): fix compilation warnings","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/f5c35f8d762f9098f61f3dfc34bd9d60a3afd2ea"},{"sha":"8ba17af50b72fcae897b084413e3595d1d31d03a","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(frontends/lean/builtin_cmds): non-determinism","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/8ba17af50b72fcae897b084413e3595d1d31d03a"},{"sha":"11043bc888d3c0ca03130dd75cc10b6dc54a4940","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"chore(frontends/lean/builtin_cmds): remove dead code","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/11043bc888d3c0ca03130dd75cc10b6dc54a4940"},{"sha":"fd0b593fba532bb381f51402a7d813502d7ba55c","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(frontends/lean): add definition_cmds files","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/fd0b593fba532bb381f51402a7d813502d7ba55c"},{"sha":"f056f0f2cbee856f22c88b977d53190134094d0d","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(library): definitional ==> constructions","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/f056f0f2cbee856f22c88b977d53190134094d0d"},{"sha":"fc4e304b277a2b4d3d6ca80ac2d8311c5fca9d1d","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(library): move equations to equations_compiler","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/fc4e304b277a2b4d3d6ca80ac2d8311c5fca9d1d"},{"sha":"09459c0d849e81e700d888068f329f5f7a799a02","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(library/equations_compiler): isolate old equations compiler","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/09459c0d849e81e700d888068f329f5f7a799a02"},{"sha":"65032fb9a434361300e6f76d170c79e4bb40dcb1","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(init/init): missing initialization","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/65032fb9a434361300e6f76d170c79e4bb40dcb1"},{"sha":"80b6bb47f8d1a7df5d8673a3ab26970cdf412e7f","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(frontends/lean): parse mutual_definition","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/80b6bb47f8d1a7df5d8673a3ab26970cdf412e7f"},{"sha":"8aebea558abb24053ec4446d008dc499555d0c78","author":{"name":"Daniel Selsam","email":"8f1d6bb0bd9093ce0d9331b3ca37599085cf96af@gmail.com"},"message":"feat(frontends/lean/inductive_cmds): scaffold for new inductive commands","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/8aebea558abb24053ec4446d008dc499555d0c78"},{"sha":"53190c38ca643926fbf67f2c26ce43a125fc26e5","author":{"name":"Daniel Selsam","email":"8f1d6bb0bd9093ce0d9331b3ca37599085cf96af@gmail.com"},"message":"feat(library/inductive): scaffold for inductive type manager","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/53190c38ca643926fbf67f2c26ce43a125fc26e5"},{"sha":"bc7e081ac147bad8117ba249e64bf56a4f1250be","author":{"name":"Daniel Selsam","email":"8f1d6bb0bd9093ce0d9331b3ca37599085cf96af@gmail.com"},"message":"feat(library/inductive_compiler): scaffold for inductive compiler","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/bc7e081ac147bad8117ba249e64bf56a4f1250be"},{"sha":"a641f9dfc08213cb2da79616adfe61724fcc5822","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(frontends/lean): add new definition command skeleton","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/a641f9dfc08213cb2da79616adfe61724fcc5822"},{"sha":"a05f803a45fcfe3ca93c9a6e79a0e70142b45e4c","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"refactor(library/equations_compiler/equations): add new headers","distinct":false,"url":"https://api.github.com/repos/dselsam/lean/commits/a05f803a45fcfe3ca93c9a6e79a0e70142b45e4c"}]}
{"actor":{"display_login":"dselsam"}}