GitHub PushEvent at 2014-05-30 23:33:42
Repository: libraries
Actor: leodemoura
Payload: {"shas":[["19085c2a60b84c52a56c6dd01e1644ce9ff4bf85","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","feat(style.md): first cut at style guidelines","Jeremy Avigad",true],["8039ddd963694f04b86cb9dff97708a21080ed61","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","feat(list.lean): start on list library","Jeremy Avigad",true],["3f421f1465c17119583bd8b776eaddb757744f3b","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","feat(equality_test.lean): experiments with equality axioms\n\nThis reduces most of the current axioms for equality and heterogeneous equality to the basic rules for Id as an inductive type, plus Pi injectivity. There are universe problems that should go away in Lean 0.2.","Jeremy Avigad",true],["f5373b24b87676b01ce7c3d70a8c1798a79569e0","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","feat(todo.md): added to do list","Jeremy Avigad",true],["700c12ac3937014858d65b109712e1e4d1238a65","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","chore(list.lean): added copyright info to header","Jeremy Avigad",true],["b94eda70fdc079212ddf34f5267a42eb4597536e","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","Added natural number libraries using inductive types with add and mul","Floris van Doorn",true],["5df03dd70befb850ec2b39ccd89ec8f09ec46572","63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","chore(.travis.yml): set up travis-ci for backup and diff notification","Soonho Kong",true],["99c1b97c13129c1a8e3294d25af10318a389cc16","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","feat(list.lean): proved reverse reverse theorem","Jeremy Avigad",true],["94788c0794428450fcd9a65fb94ff56ca43657b5","2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","Merge branch 'master' of github.com:leanprover/libraries","Jeremy Avigad",true],["11fba890bf0a3a61311f2ccd702c11ec9ed53b98","63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","chore(Makefile): add Makefile\n\nAdd simple 'Makefile' to compile '.lean' files into '.olean'\nfiles. It assumes that 'lean' is in the 'PATH' variable. If this is\nnot the case, you can run 'make' while specifying the pathname for\n'lean' as follows:\n\n    $ make LEAN=~/work/lean0.1/build/shell/lean","Soonho Kong",true],["9028d190dd1513c937e5a4d99133883944e7cda2","63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","chore(.travis.yml): compile .lean to .olean and upload to dropbox","Soonho Kong",true],["1a4df9bcfbf5fd1d900636abc487edcb7fc15959","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","feat(nat/kernel)\nAdded le lt and a bunch of theorems\nSome theorems still need a proof and are currently and axiom. nat_ind currently only compiles with the standard kernel, not the kernel in this folder","Floris van Doorn",true],["941dc508ff02f13ff73f65fd645d5deb636656db","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","feat(nat): Add le/lt","Floris van Doorn",true],["c469fcad0b5b34b1d4158181f43705241003e003","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","feat(nat): use new kernel\nchange proofs to be compatible with the kenrel in this library, and prove some more theorems","Floris van Doorn",true],["151336e966d2de3b2e03387a76cf3af1fc9dc7e3","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","chore(makefile): use -n and compile in right order","Floris van Doorn",true],["cd98fe11c9093311822c60886d7facdf52800e7d","240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","chore(makefile/list): fix makefile and convert list to use nat","Floris van Doorn",true],["2df9442ce5e4f2329bd617133b7ba00f22ce9c81","63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","chore(library/standard): fix permission","Soonho Kong",true],["91048cf64a2fc28669efe78e56d81e828d610377","63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","chore(Makefile): add and use extract_deps in Makefile","Soonho Kong",true],["22c6130c739b64618e2792b76bb3d1687865d72e","63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","chore(library/standard/extract_dep): add EXCEPT to specify deps which do not need compilation","Soonho Kong",true],["8448085f1649e809083cb42a2c501f539494db7a","63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","fix(library/standard/equality_test): add \"import kernel\"","Soonho Kong",true]],"size":29,"ref":"refs/heads/master","head":"99cbfd0359579eceaf5ed9d4e36597976ef69f48"}