{"push_id":912798727,"size":11,"distinct_size":11,"ref":"refs/heads/master","head":"84cdf3d36d401bc2855de3a0530601647b49c592","before":"45725211aef3138f346eec011aa5093b988c0d5c","commits":[{"sha":"f1daf8f24e0a48cc746f9238c8348b23b989e688","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"fix(algebra/group.lean): remove unnecessary use of add.assoc from theorem bit0_add_bit1_helper","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/f1daf8f24e0a48cc746f9238c8348b23b989e688"},{"sha":"0e3b13f1a0e80c893136be2debe8ee6a65742e82","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"refactor(library/algebra): combine group_bigops and group_set_bigops","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/0e3b13f1a0e80c893136be2debe8ee6a65742e82"},{"sha":"baf11d0018b285a200661c050c9c9527de027a44","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/algebra/ring_bigops): make start on file with more properties of sums and products","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/baf11d0018b285a200661c050c9c9527de027a44"},{"sha":"8ccafc426778297eacb280dc7481291f18429e38","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"fix(library/init/function): fix typo","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/8ccafc426778297eacb280dc7481291f18429e38"},{"sha":"8d50405e682fbe123cceaec1a1ba80f85bd52c5e","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"chore(library/extras/latex/lstlean.text): update lists for syntax highlighting","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/8d50405e682fbe123cceaec1a1ba80f85bd52c5e"},{"sha":"68ecdc4c26cca38247dc1eebdf6d29cb571e3bf7","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(src/emacs/README.md): expand instructions slightly","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/68ecdc4c26cca38247dc1eebdf6d29cb571e3bf7"},{"sha":"6913eb0c768d65260c2857a7d6c6c0d6095bacf5","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"refactor(library/init/subtype.lean): put subtype notation in the namespace\n\nThe notation { x : A | P x } is overloaded in set, and is ambiguous.","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/6913eb0c768d65260c2857a7d6c6c0d6095bacf5"},{"sha":"dc8cad10bf8f9f97d285b9a2cfdf07ed57d3973a","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(src/emacs/README.md): add header","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/dc8cad10bf8f9f97d285b9a2cfdf07ed57d3973a"},{"sha":"5b3fbf161827c1f886e93dd730fc358dff8e743d","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/algebra/module): make a start on modules and vector spaces (with material from Nathaniel Thomas)","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/5b3fbf161827c1f886e93dd730fc358dff8e743d"},{"sha":"08fbf127c61ce164cbcd523d6f79a067e250b9bd","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/analysis/metric_space,real_limit): define complete metric space, make real an instance","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/08fbf127c61ce164cbcd523d6f79a067e250b9bd"},{"sha":"84cdf3d36d401bc2855de3a0530601647b49c592","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(library/theories/analysis/normed_space): start theory of normed spaces for analysis","distinct":true,"url":"https://api.github.com/repos/avigad/lean/commits/84cdf3d36d401bc2855de3a0530601647b49c592"}]}