{"push_id":875259855,"size":17,"distinct_size":9,"ref":"refs/heads/master","head":"bb95717453b7b6ecc616af73cd45ca474cf25916","before":"8c0153b3893c21aaf85564104a73f635e606d37d","commits":[{"sha":"bab88c6321cadf5cd9efc4af2f72e55b7d200a0d","author":{"email":"240eaf9b7dd8bf34824fa6213c6ea24402f09b79@andrew.cmu.edu","name":"Floris van Doorn"},"message":"feat(A1): add some information to the Quick Reference","distinct":false,"url":"https://api.github.com/repos/avigad/tutorial/commits/bab88c6321cadf5cd9efc4af2f72e55b7d200a0d"},{"sha":"da83c0784d4a209b75f17363b4736876e4d3c4b4","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"fix(README.md): add texlive-luatex\n\nclose #142","distinct":false,"url":"https://api.github.com/repos/avigad/tutorial/commits/da83c0784d4a209b75f17363b4736876e4d3c4b4"},{"sha":"dcf9c39928d34310e01991b5ddce55f656eb7bb1","author":{"email":"c8add0dc2d9f355f4b4c51cd59b2ffcf600e29a6@andrew.cmu.edu","name":"Rob Lewis"},"message":"fix(A1): typos, style","distinct":false,"url":"https://api.github.com/repos/avigad/tutorial/commits/dcf9c39928d34310e01991b5ddce55f656eb7bb1"},{"sha":"fecd385a14414eb7597321fb2cd3801979238b04","author":{"email":"597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com","name":"Rob Lewis"},"message":"fix(12): typos","distinct":false,"url":"https://api.github.com/repos/avigad/tutorial/commits/fecd385a14414eb7597321fb2cd3801979238b04"},{"sha":"874ce41c459b05a59503db7828a76dbb2fb7f1fc","author":{"email":"9fa90f705a05b3ea78de773b4d35179fa84f34f9@gmail.com","name":"Christopher Mazey"},"message":"fix(03): remove duplicate exercise\n\nThe tutorial states that exercises requiring classical reasoning are\ngrouped at the end; this exercise is repeated twice, and appears in the\nwrong group.","distinct":false,"url":"https://api.github.com/repos/avigad/tutorial/commits/874ce41c459b05a59503db7828a76dbb2fb7f1fc"},{"sha":"7066f864c2075b44950d749e73d3c8f3423f6a32","author":{"email":"9fa90f705a05b3ea78de773b4d35179fa84f34f9@gmail.com","name":"Christopher Mazey"},"message":"fix(04): typos\n\nI believe the parentheses are necessary here, otherwise the exercise is\nimpossible.  (It amounts to showing r from just A -> r, knowing nothing\nof A.)","distinct":false,"url":"https://api.github.com/repos/avigad/tutorial/commits/7066f864c2075b44950d749e73d3c8f3423f6a32"},{"sha":"3884d70bcd8c676826281daf88fcf56aa72654b2","author":{"email":"9fa90f705a05b3ea78de773b4d35179fa84f34f9@gmail.com","name":"Christopher Mazey"},"message":"fix(04): typo\n\nremove \"the type of.\"  It is the case that the Pi type is an element of\nthe type, not that the type of the Pi type is.","distinct":false,"url":"https://api.github.com/repos/avigad/tutorial/commits/3884d70bcd8c676826281daf88fcf56aa72654b2"},{"sha":"40a02ef9bbaf715d789f13485ca57827561b04dd","author":{"email":"9fa90f705a05b3ea78de773b4d35179fa84f34f9@gmail.com","name":"Christopher Mazey"},"message":"fix(04): typo\n\nswap the nots","distinct":false,"url":"https://api.github.com/repos/avigad/tutorial/commits/40a02ef9bbaf715d789f13485ca57827561b04dd"},{"sha":"932e2f500b3f6517c30d63e97bfab8b4d4dc0e7a","author":{"email":"63adb5ce2831ba4d8e937ce6b96c4b96780c2933@cs.cmu.edu","name":"Soonho Kong"},"message":"fix(elisp/org-pdf-export.el): update smart-quote following updates in org-8.3.2\n\nSee: https://lists.nongnu.org/archive/html/emacs-orgmode/2015-10/msg00087.html","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/932e2f500b3f6517c30d63e97bfab8b4d4dc0e7a"},{"sha":"b36fc176559af099f02c79786e2dc626fd69ca12","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"fix(*): adapt to new typeclasses","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/b36fc176559af099f02c79786e2dc626fd69ca12"},{"sha":"c4d5282367d2f4c5cc90fdb80627cf6a82f94ce4","author":{"email":"04eee3258902297ef5081ba8b0786f6ab1274795@gmail.com","name":"Floris van Doorn"},"message":"fix(A1): typo","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/c4d5282367d2f4c5cc90fdb80627cf6a82f94ce4"},{"sha":"9ad9901ceb03e587a97e6dbabd89aa3165f1f82a","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"fix(02,10): fix typo, and establish type for generic numerals","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/9ad9901ceb03e587a97e6dbabd89aa3165f1f82a"},{"sha":"5015df4797117c62bd25eb8bd737cd39a2ce548a","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"feat(04): add an example of a structured proof, that sqrt 2 is irrational","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/5015df4797117c62bd25eb8bd737cd39a2ce548a"},{"sha":"6b500ab5acffb965a30152892cf56586a2519e1d","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"fix(05): correct discussion of overloading, add examples","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/6b500ab5acffb965a30152892cf56586a2519e1d"},{"sha":"0f8a1822452cd001b21115d93b2f34f8ed5c06ae","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"refactor(04): clarify exercises with existential quantifier","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/0f8a1822452cd001b21115d93b2f34f8ed5c06ae"},{"sha":"5c3a19376c18aa10314c509eaf0ee66f63f27214","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"refactor(A1): reformat explanation of by+, begin+","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/5c3a19376c18aa10314c509eaf0ee66f63f27214"},{"sha":"bb95717453b7b6ecc616af73cd45ca474cf25916","author":{"email":"2a91c65c6d7f63ca829e9eea8bea6b5c6ae36bd9@cmu.edu","name":"Jeremy Avigad"},"message":"fix(02,05,08,09): adapt to changes in the library","distinct":true,"url":"https://api.github.com/repos/avigad/tutorial/commits/bb95717453b7b6ecc616af73cd45ca474cf25916"}]}