{"push_id":668936730,"size":4,"distinct_size":4,"ref":"refs/heads/master","head":"8ce992b0772592a1aa8c47780e07a4291149b0de","before":"3e87f09d7890d98ebd6cf380d4a87c86130a5e73","commits":[{"sha":"5f628d5080a88b96c1f299b3e45c7f050ab0acd9","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean/builtin_exprs): allow 'calc' expressions to be used in tactic mode","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/5f628d5080a88b96c1f299b3e45c7f050ab0acd9"},{"sha":"1665ee39e8f75453eff3f751de6ec36b6b02992a","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/data/finset/card): test 'induction' tactic at finset","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/1665ee39e8f75453eff3f751de6ec36b6b02992a"},{"sha":"c133d2650537172cbbbc9592878f3d401a99e77b","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean/builtin_exprs): change how 'show' is processed in tactics\n\nUnresolved placeholders were not being reported","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/c133d2650537172cbbbc9592878f3d401a99e77b"},{"sha":"8ce992b0772592a1aa8c47780e07a4291149b0de","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(frontends/lean/builtin_exprs): allow 'obtain' to be used in tactic mode","distinct":true,"url":"https://api.github.com/repos/leodemoura/lean/commits/8ce992b0772592a1aa8c47780e07a4291149b0de"}]}