{"push_id":1061099539,"size":26,"distinct_size":26,"ref":"refs/heads/master","head":"933b5863cd4e9fc06dad97225b0bd060935dfe85","before":"226f8bafeb9baaa5a2ac58000c83d6beb29991e2","commits":[{"sha":"73271ac2c98f0c88211b82087dd8292d48e4305d","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/move.lean): add facts to move in Lean 3","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/73271ac2c98f0c88211b82087dd8292d48e4305d"},{"sha":"c0720d69e3e632a94c041ab65b4d6119e83ccca5","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/topology/continuous.lean): add theorems about continuous functions (includes work by Jacob Gross)","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/c0720d69e3e632a94c041ab65b4d6119e83ccca5"},{"sha":"ef982d9ad63a7575a131020e75bc6cf1eb571564","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"refactor(library/theories/analysis/metric_space.lean): use new definition of continuous_at","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/ef982d9ad63a7575a131020e75bc6cf1eb571564"},{"sha":"1f967695a8b0d13d3db9d7ad280014788fa92cfe","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/measure_theory/sigma_algebra): add measurable and borel functions, from Jacob Gross","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/1f967695a8b0d13d3db9d7ad280014788fa92cfe"},{"sha":"543d7702f0fb5547e4dc2aafc726aa7062c54478","author":{"email":"c9a384dcc63529a27b380881c4e27dace2499077@nullri.ch","name":"Sebastian Ullrich"},"message":"fix(shell/lean): fix documentation of some cmdline options","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/543d7702f0fb5547e4dc2aafc726aa7062c54478"},{"sha":"08c55754a9f5ceae311b5191c87505a71351477a","author":{"email":"c9a384dcc63529a27b380881c4e27dace2499077@nullri.ch","name":"Sebastian Ullrich"},"message":"fix(emacs/lean-mode.el): invoke lean from project root if existent","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/08c55754a9f5ceae311b5191c87505a71351477a"},{"sha":"5810a4de8fd27dd24efd3b766bee740065e9fb1c","author":{"email":"c9a384dcc63529a27b380881c4e27dace2499077@nullri.ch","name":"Sebastian Ullrich"},"message":"fix(emacs/lean-server.el): invoke lean --server from project root if existent","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/5810a4de8fd27dd24efd3b766bee740065e9fb1c"},{"sha":"b1ed69f621438c7c28ba0165e529710cf0adcf0f","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(hott): small changes, mostly in pointed2","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/b1ed69f621438c7c28ba0165e529710cf0adcf0f"},{"sha":"05b59aecf8f37423db6735b8419cec00c2b3d8da","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"refactor(hott): rename apd to apdt","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/05b59aecf8f37423db6735b8419cec00c2b3d8da"},{"sha":"80a2e285cb53ce7c98b1bd56a90a4a284994ff60","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(init/ua): add ua_symm and ua_trans","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/80a2e285cb53ce7c98b1bd56a90a4a284994ff60"},{"sha":"dc37ec954d18d4c74350cadec0d49de55dec41bd","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"refactor(hott): rename apdo to apd","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/dc37ec954d18d4c74350cadec0d49de55dec41bd"},{"sha":"3240df602092cb5c59c6828353383d5bf925f060","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(book): add comments about chapter 10","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/3240df602092cb5c59c6828353383d5bf925f060"},{"sha":"3887efa7c13fb4103a7eb75cad3c194de8a31fd7","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(hott): some renamings in init.path","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/3887efa7c13fb4103a7eb75cad3c194de8a31fd7"},{"sha":"54da5bcbda7421433e5cb00cb4a1279c086d6d55","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(hott): add some [constructor] attributes","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/54da5bcbda7421433e5cb00cb4a1279c086d6d55"},{"sha":"4895726c54163325be638b3ed1dcf403968367a9","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(connectedness): show that if f is n-connected, then trunc_functor k f is so, too","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/4895726c54163325be638b3ed1dcf403968367a9"},{"sha":"f983724cf6310b9ecc9f06d208ff4439f939bb9d","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(pointed): merge pointed2 into pointed\n\nWe move the basic notions of pointed types into init.pointed, to avoid cycles in the import graph. Also adds pointed versions of pi and sigma, with corresponding notation","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/f983724cf6310b9ecc9f06d208ff4439f939bb9d"},{"sha":"a6319118e384a3d6475ec3cb93ac1f733b69ae08","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(types.pointed): small additions","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/a6319118e384a3d6475ec3cb93ac1f733b69ae08"},{"sha":"7a9e1c7f4f820d05081ecb8cab7babcd8dc8c369","author":{"email":"dbf64074c535b6b84a73384ad297d5521819740f@web.de","name":"Jakob von Raumer"},"message":"chore(hott) fix sum proof by adding manual coercions","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/7a9e1c7f4f820d05081ecb8cab7babcd8dc8c369"},{"sha":"651df51cb722266553bba5d6f3cfe0b7b9ed6c80","author":{"email":"dbf64074c535b6b84a73384ad297d5521819740f@web.de","name":"Jakob von Raumer"},"message":"chore(hott) the coercion doesn't seem to be the problem","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/651df51cb722266553bba5d6f3cfe0b7b9ed6c80"},{"sha":"b7a25a249a55af2b3889b76c9562bb293c31efeb","author":{"email":"597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com","name":"Rob Lewis"},"message":"feat(library/algebra): define matrices, prove Farkas' lemma","distinct":true,"url":"https://api.github.com/repos/leanprover/lean/commits/b7a25a249a55af2b3889b76c9562bb293c31efeb"}]}