GitHub PushEvent at 2014-12-04 00:38:05
Repository: lean
Actor: fpvandoorn
Payload: {"shas":[["5b2d17e4abb1965b40fc789d4419e6c588910686","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(frontends/lean): add 'print notation' command","Leonardo de Moura",true],["73429547baf931c92d8259e68126dea808745306","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(init/reserved_notation): remove \"invisible\" character at `\\/`","Leonardo de Moura",true],["1b135625913a281f22cfb0644f267f33a352fcb8","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(library/flycheck): crash when io_state_stream is destroyed before flycheck_scope","Leonardo de Moura",true],["1bffd8dd215e3a796344b5e5ad95ed999d173943","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","refactor(library/algebra/order): change strong order pair, adopt new naming conventions","Jeremy Avigad",true],["57effaf1a9803e2bfa169d2b7c6581180e7e2a05","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","refactor(library/algebra): use new naming conventions, add information to speed up proofs","Jeremy Avigad",true],["050104cdfda29f303c403c288686a7641eb7edb5","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(library/unifier): assertion violation","Leonardo de Moura",true],["f948241bb910529658a268229b45bb25b0bdb4da","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(library/definitional): add auxiliary functions","Leonardo de Moura",true],["fca97d5bb219aa29d2f186695e09f0eee87c8634","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(library/definitional): add brec_on construction, closes #272","Leonardo de Moura",true],["0443c1e70cfa9e6632958750af05c10c0c0e521c","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","fix(frontends/lean): intro tactic + universe variables, fixes #362","Leonardo de Moura",true],["d10bb92a7d6c9c35418d9799617cc622ebe12e34","7610bae85f2b530654cc716772f1fe653373e892@microsoft.com","feat(library/aliases): protected definitions in nested namespaces, closes #331","Leonardo de Moura",true],["939448d083f20bb29f55a6326784b031e8339407","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","feat(library/algebra): modify categories to use definitions, prove basic theorems about discrete categories","Floris van Doorn",true],["9b46e9eb6fea4327e93ecb5599f253e3a3585932","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","fix(hott/trunc): add explicit coercion so that the notation works if nat is not opened","Floris van Doorn",true],["3dcb1dce0911beb3657e2e802d9b296e31def795","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","style(hott/path): indent within namespace, add variables","Floris van Doorn",true],["d94c537321623d2d02aed362fea60e925647ef04","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","style(hott/types): some style fixes in prod and sigma","Floris van Doorn",true],["1ffaef83607eaf55ebdcd3ba9c08733db50d576b","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","feat(hott/types): start characterization of pi-types and W-types","Floris van Doorn",true]],"size":15,"ref":"refs/heads/master","head":"1ffaef83607eaf55ebdcd3ba9c08733db50d576b"}