{"action":"created","issue":{"url":"https://api.github.com/repos/snu-sf-class/pl201602/issues/9","repository_url":"https://api.github.com/repos/snu-sf-class/pl201602","labels_url":"https://api.github.com/repos/snu-sf-class/pl201602/issues/9/labels{/name}","comments_url":"https://api.github.com/repos/snu-sf-class/pl201602/issues/9/comments","events_url":"https://api.github.com/repos/snu-sf-class/pl201602/issues/9/events","html_url":"https://github.com/snu-sf-class/pl201602/issues/9","id":179027074,"number":9,"title":"[Error Nat Type] Error when try to execute a instruction with a nat type","user":{"login":"sebspas","id":10104348,"avatar_url":"https://avatars.githubusercontent.com/u/10104348?v=3","gravatar_id":"","url":"https://api.github.com/users/sebspas","html_url":"https://github.com/sebspas","followers_url":"https://api.github.com/users/sebspas/followers","following_url":"https://api.github.com/users/sebspas/following{/other_user}","gists_url":"https://api.github.com/users/sebspas/gists{/gist_id}","starred_url":"https://api.github.com/users/sebspas/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sebspas/subscriptions","organizations_url":"https://api.github.com/users/sebspas/orgs","repos_url":"https://api.github.com/users/sebspas/repos","events_url":"https://api.github.com/users/sebspas/events{/privacy}","received_events_url":"https://api.github.com/users/sebspas/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-09-24T12:05:59Z","updated_at":"2016-09-24T13:18:58Z","closed_at":null,"body":"Hi,\r\n\r\nI tried to do some training on coq, but when i define this : \r\n`Inductive nat : Type := \r\n  | O : nat\r\n  | S : nat -> nat.\r\n\r\nCheck (S (S (S (S O)))).`\r\n\r\ni don't get 4 as printed... Also when i try this : \r\n`Compute (minusTwo 4).`\r\nI get this error : \r\n\r\n> Error: The term \"4\" has type \"Datatypes.nat\" while it is expected to have type \"nat\".\r\n\r\nI think it's because coq already includen a Datatypes module....\r\n\r\nThanks for your help."},"comment":{"url":"https://api.github.com/repos/snu-sf-class/pl201602/issues/comments/249364461","html_url":"https://github.com/snu-sf-class/pl201602/issues/9#issuecomment-249364461","issue_url":"https://api.github.com/repos/snu-sf-class/pl201602/issues/9","id":249364461,"user":{"login":"sebspas","id":10104348,"avatar_url":"https://avatars.githubusercontent.com/u/10104348?v=3","gravatar_id":"","url":"https://api.github.com/users/sebspas","html_url":"https://github.com/sebspas","followers_url":"https://api.github.com/users/sebspas/followers","following_url":"https://api.github.com/users/sebspas/following{/other_user}","gists_url":"https://api.github.com/users/sebspas/gists{/gist_id}","starred_url":"https://api.github.com/users/sebspas/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/sebspas/subscriptions","organizations_url":"https://api.github.com/users/sebspas/orgs","repos_url":"https://api.github.com/users/sebspas/repos","events_url":"https://api.github.com/users/sebspas/events{/privacy}","received_events_url":"https://api.github.com/users/sebspas/received_events","type":"User","site_admin":false},"created_at":"2016-09-24T13:18:58Z","updated_at":"2016-09-24T13:18:58Z","body":"Just make working 'Compute (minusTwo 4)' as well as 'Compute (minusTwo S(S(S(O))))'\r\n"}}
{"actor":{"display_login":"sebspas"}}