{"push_id":794552283,"size":11,"distinct_size":11,"ref":"refs/heads/master","head":"631b9b3312e8c2f3be767574d2bcbbeb37c8414a","before":"352a906ba2d7fb3c344eace99a969e486ea091c2","commits":[{"sha":"00a59a50b6b87a0c52aa2a8c52b6138ae594f189","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"feat(library/context): add \"context\"-like object","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/00a59a50b6b87a0c52aa2a8c52b6138ae594f189"},{"sha":"46f7123cc8b4ff3c3cc67c719b3ce71bdbd35ef6","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"fix(runtime/cpp): typo","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/46f7123cc8b4ff3c3cc67c719b3ce71bdbd35ef6"},{"sha":"1259f52fa8ad2ccd03b190b59993b5e993082f89","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(runtime/cpp/lean_runtime): add assertion to make sure we are satisfying alignment constraints","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/1259f52fa8ad2ccd03b190b59993b5e993082f89"},{"sha":"5028d794ce79f70a5acd060368bfa17e3ce54a86","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"refactor(library,library/blast): move context to blast","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/5028d794ce79f70a5acd060368bfa17e3ce54a86"},{"sha":"b7271c39af71b474c56baf179cc3b15f8492f20b","author":{"email":"7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","name":"Leonardo de Moura"},"message":"chore(library/blast,runtime/cpp): fix style","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/b7271c39af71b474c56baf179cc3b15f8492f20b"},{"sha":"f4fa38e36597f4beaa22cb7c443dfe9f8a31768a","author":{"email":"597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com","name":"Rob Lewis"},"message":"chore(library/data/{rat, pnat}): move theorems from reals to more appropriate places","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/f4fa38e36597f4beaa22cb7c443dfe9f8a31768a"},{"sha":"4312f1e54ba55bcb8c00310a788aef33e08352af","author":{"email":"597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com","name":"Rob Lewis"},"message":"chore(library/data/real): clean and rename theorems in completeness proofs","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/4312f1e54ba55bcb8c00310a788aef33e08352af"},{"sha":"f5dcb1e0a9a9c356526c130c02a80a6fc62b1621","author":{"email":"597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com","name":"Rob Lewis"},"message":"feat(library/algebra): add missing theorems to algebra library","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/f5dcb1e0a9a9c356526c130c02a80a6fc62b1621"},{"sha":"ea3915f279dc0e0368b5b7d746a80428fdad7ce2","author":{"email":"597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com","name":"Rob Lewis"},"message":"feat(library/theories/analysis): prove intermediate value theorem","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/ea3915f279dc0e0368b5b7d746a80428fdad7ce2"},{"sha":"ee257a7c6c4d9d0e7a6c44f1c00a6001300642d0","author":{"email":"c8add0dc2d9f355f4b4c51cd59b2ffcf600e29a6@andrew.cmu.edu","name":"Rob Lewis"},"message":"chore(library/data/{nat,real}): rename and move iterate function","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/ee257a7c6c4d9d0e7a6c44f1c00a6001300642d0"},{"sha":"631b9b3312e8c2f3be767574d2bcbbeb37c8414a","author":{"email":"c8add0dc2d9f355f4b4c51cd59b2ffcf600e29a6@andrew.cmu.edu","name":"Rob Lewis"},"message":"feat(library/theories/analysis): clean and simplify proof of IVT","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/631b9b3312e8c2f3be767574d2bcbbeb37c8414a"}]}