{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/257","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/257/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/257/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/257/events","html_url":"https://github.com/UniMath/UniMath/pull/257","id":121546154,"number":257,"title":"Rational number computation","user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":17,"created_at":"2015-12-10T18:13:55Z","updated_at":"2016-07-09T14:31:24Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/UniMath/UniMath/pulls/257","html_url":"https://github.com/UniMath/UniMath/pull/257","diff_url":"https://github.com/UniMath/UniMath/pull/257.diff","patch_url":"https://github.com/UniMath/UniMath/pull/257.patch"},"body":"This resolves #244.\r\n\r\nNote: this does not make 1/2 = 3/6 in Q provable by reflexivity.\r\n\r\nIt also renames \"hsubtypes\" to \"subtype\" and \"submonoids\" to \"submonoid\".  (The plural is\r\ncounterintuitive.)\r\n\r\nI also introduce a way to use a proof of decidable equality to prove equations, and apply it to\r\nhq in Dedekind:\r\n```\r\nLemma hq2eq1plus1 : 2 = 1 + 1.\r\n  Proof.\r\n -  rewrite <- hztohqand1, <- nattohzand1.\r\n -  now rewrite <- hztohqandplus, <- nattohzandplus.\r\n +  exact (confirm_pos (hqdeceq, 2, 1+1)).\r\n  Qed.\r\n```\r\n"},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/231537077","html_url":"https://github.com/UniMath/UniMath/pull/257#issuecomment-231537077","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/257","id":231537077,"user":{"login":"vladimirias","id":424011,"avatar_url":"https://avatars.githubusercontent.com/u/424011?v=3","gravatar_id":"","url":"https://api.github.com/users/vladimirias","html_url":"https://github.com/vladimirias","followers_url":"https://api.github.com/users/vladimirias/followers","following_url":"https://api.github.com/users/vladimirias/following{/other_user}","gists_url":"https://api.github.com/users/vladimirias/gists{/gist_id}","starred_url":"https://api.github.com/users/vladimirias/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/vladimirias/subscriptions","organizations_url":"https://api.github.com/users/vladimirias/orgs","repos_url":"https://api.github.com/users/vladimirias/repos","events_url":"https://api.github.com/users/vladimirias/events{/privacy}","received_events_url":"https://api.github.com/users/vladimirias/received_events","type":"User","site_admin":false},"created_at":"2016-07-09T14:31:24Z","updated_at":"2016-07-09T14:31:24Z","body":"While you are at it could you please remove the comment \"The coconus behaves like the image of a function.\" from the line 854 of PartA. The coconus does not behave like the image. "}}
{"actor":{"display_login":"vladimirias"}}