{"push_id":1415148426,"size":7,"distinct_size":7,"ref":"refs/heads/lean3","head":"19596eae778bdc08ffef1e54448e905b71a4da3c","before":"ed2a507dd947d145bf32565d07adcffb47365a4d","commits":[{"sha":"c6179721a46b025ff59ceecb68f20b7276e794c8","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(library/library.md): stray keystroke","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/c6179721a46b025ff59ceecb68f20b7276e794c8"},{"sha":"227e16ea6ba0082c91bcec172a3bf585e0521c96","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library): add mk_nat_val_ne_proof\n\nProcedure for building an efficient disequality proof for natural\nnumber values encoded in binary.","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/227e16ea6ba0082c91bcec172a3bf585e0521c96"},{"sha":"88b2af3b65ff3b22df0a56867c06d2789946d97f","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/meta/interactive): add 'exfalso'","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/88b2af3b65ff3b22df0a56867c06d2789946d97f"},{"sha":"a8267a8e412df89835b8c1d982b1503ccfbb4836","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"feat(library/init/nat_lemmas): add more lemmas needed by basic automation","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/a8267a8e412df89835b8c1d982b1503ccfbb4836"},{"sha":"e17b3df16adf012bdf7c9bd2f7e01f86898f88a5","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"fix(frontends/lean/elaborator): bad error message","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/e17b3df16adf012bdf7c9bd2f7e01f86898f88a5"},{"sha":"1c484e8926766dc28b03373200eaba26e5675c10","author":{"name":"Leonardo de Moura","email":"ba10aed3432723ba43fa2d8fb44aba9979912a8a@microsoft.com"},"message":"chore(tests/lean/run): adjust tests","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/1c484e8926766dc28b03373200eaba26e5675c10"},{"sha":"19596eae778bdc08ffef1e54448e905b71a4da3c","author":{"name":"Daniel Selsam","email":"8f1d6bb0bd9093ce0d9331b3ca37599085cf96af@gmail.com"},"message":"fix(library/init/logic.lean): if_true and if_false take instance as implicit instead of inst_implicit","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/19596eae778bdc08ffef1e54448e905b71a4da3c"}]}
{"actor":{"display_login":"leodemoura"}}