{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/254","repository_url":"https://api.github.com/repos/leanprover/mathlib","labels_url":"https://api.github.com/repos/leanprover/mathlib/issues/254/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/mathlib/issues/254/comments","events_url":"https://api.github.com/repos/leanprover/mathlib/issues/254/events","html_url":"https://github.com/leanprover/mathlib/pull/254","id":350201681,"node_id":"MDExOlB1bGxSZXF1ZXN0MjA4MTA5OTI2","number":254,"title":"feat(data/rat): inhabited rationals","user":{"login":"kbuzzard","id":31867827,"node_id":"MDQ6VXNlcjMxODY3ODI3","avatar_url":"https://avatars3.githubusercontent.com/u/31867827?v=4","gravatar_id":"","url":"https://api.github.com/users/kbuzzard","html_url":"https://github.com/kbuzzard","followers_url":"https://api.github.com/users/kbuzzard/followers","following_url":"https://api.github.com/users/kbuzzard/following{/other_user}","gists_url":"https://api.github.com/users/kbuzzard/gists{/gist_id}","starred_url":"https://api.github.com/users/kbuzzard/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kbuzzard/subscriptions","organizations_url":"https://api.github.com/users/kbuzzard/orgs","repos_url":"https://api.github.com/users/kbuzzard/repos","events_url":"https://api.github.com/users/kbuzzard/events{/privacy}","received_events_url":"https://api.github.com/users/kbuzzard/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-08-13T21:31:27Z","updated_at":"2018-08-13T21:36:07Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/leanprover/mathlib/pulls/254","html_url":"https://github.com/leanprover/mathlib/pull/254","diff_url":"https://github.com/leanprover/mathlib/pull/254.diff","patch_url":"https://github.com/leanprover/mathlib/pull/254.patch"},"body":"TO CONTRIBUTORS:\r\n\r\nMake sure you have:\r\n\r\n * [ ] reviewed and applied the coding style: [coding](./docs/style.md), [naming](./docs/naming.md)\r\n * [ ] for tactics:\r\n     * [ ] added or adapted documentation in [tactics.md](./docs/tactics.md)\r\n     * [ ] write an example of use of the new feature in [tactics.lean](./tests/tactics.lean)\r\n  * [x] make sure definitions and lemmas are put in the right files\r\n  * [x] make sure definitions and lemmas are not redundant\r\n\r\nFor reviewers: [code review check list](./docs/code-review.md)\r\n\r\nRationals now inhabited."},"comment":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/comments/412673132","html_url":"https://github.com/leanprover/mathlib/pull/254#issuecomment-412673132","issue_url":"https://api.github.com/repos/leanprover/mathlib/issues/254","id":412673132,"node_id":"MDEyOklzc3VlQ29tbWVudDQxMjY3MzEzMg==","user":{"login":"bryangingechen","id":5209952,"node_id":"MDQ6VXNlcjUyMDk5NTI=","avatar_url":"https://avatars3.githubusercontent.com/u/5209952?v=4","gravatar_id":"","url":"https://api.github.com/users/bryangingechen","html_url":"https://github.com/bryangingechen","followers_url":"https://api.github.com/users/bryangingechen/followers","following_url":"https://api.github.com/users/bryangingechen/following{/other_user}","gists_url":"https://api.github.com/users/bryangingechen/gists{/gist_id}","starred_url":"https://api.github.com/users/bryangingechen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bryangingechen/subscriptions","organizations_url":"https://api.github.com/users/bryangingechen/orgs","repos_url":"https://api.github.com/users/bryangingechen/repos","events_url":"https://api.github.com/users/bryangingechen/events{/privacy}","received_events_url":"https://api.github.com/users/bryangingechen/received_events","type":"User","site_admin":false},"created_at":"2018-08-13T21:36:07Z","updated_at":"2018-08-13T21:36:07Z","author_association":"NONE","body":"Would it make sense to also include some of the long sequences of \"extra instances\" à la https://github.com/leanprover/mathlib/blob/master/data/real/basic.lean#L75 ?"}}
{"actor":{"display_login":"bryangingechen"}}