{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/423","labels_url":"https://api.github.com/repos/leanprover/lean/issues/423/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/423/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/423/events","html_url":"https://github.com/leanprover/lean/pull/423","id":56412077,"number":423,"title":"new theorems in library/data/nat/div, and minor corrections to /src/emacs/README.md","user":{"login":"avigad","id":2783534,"avatar_url":"https://avatars.githubusercontent.com/u/2783534?v=3","gravatar_id":"","url":"https://api.github.com/users/avigad","html_url":"https://github.com/avigad","followers_url":"https://api.github.com/users/avigad/followers","following_url":"https://api.github.com/users/avigad/following{/other_user}","gists_url":"https://api.github.com/users/avigad/gists{/gist_id}","starred_url":"https://api.github.com/users/avigad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/avigad/subscriptions","organizations_url":"https://api.github.com/users/avigad/orgs","repos_url":"https://api.github.com/users/avigad/repos","events_url":"https://api.github.com/users/avigad/events{/privacy}","received_events_url":"https://api.github.com/users/avigad/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-02-03T17:48:44Z","updated_at":"2015-02-03T18:15:16Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/leanprover/lean/pulls/423","html_url":"https://github.com/leanprover/lean/pull/423","diff_url":"https://github.com/leanprover/lean/pull/423.diff","patch_url":"https://github.com/leanprover/lean/pull/423.patch"},"body":"\r\nThe emacs README file begins with a section \"Requirements\" that tells the user that certain packages are needed. I would like to add the following sentence to the end of that section:\r\n\r\n\"Both the optional and required packages will be installed for you automatically the first time you use ``lean-mode``, if you follow the installation instructions below.\"\r\n\r\nIs that o.k.? It will save users from thinking that they have to install them manually.\r\n\r\nAlso: I have been adopting the practice of writing \"Lean\" instead of \"lean\", except for the syntax of commands.\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/72703592","html_url":"https://github.com/leanprover/lean/pull/423#issuecomment-72703592","issue_url":"https://api.github.com/repos/leanprover/lean/issues/423","id":72703592,"user":{"login":"avigad","id":2783534,"avatar_url":"https://avatars.githubusercontent.com/u/2783534?v=3","gravatar_id":"","url":"https://api.github.com/users/avigad","html_url":"https://github.com/avigad","followers_url":"https://api.github.com/users/avigad/followers","following_url":"https://api.github.com/users/avigad/following{/other_user}","gists_url":"https://api.github.com/users/avigad/gists{/gist_id}","starred_url":"https://api.github.com/users/avigad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/avigad/subscriptions","organizations_url":"https://api.github.com/users/avigad/orgs","repos_url":"https://api.github.com/users/avigad/repos","events_url":"https://api.github.com/users/avigad/events{/privacy}","received_events_url":"https://api.github.com/users/avigad/received_events","type":"User","site_admin":false},"created_at":"2015-02-03T18:15:16Z","updated_at":"2015-02-03T18:15:16Z","body":"\r\nI just made this change. I added \"Closes #423\" to the commit  message -- we'll see if that works (I have never tried it before)."}}