{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/79","labels_url":"https://api.github.com/repos/coq/coq/issues/79/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/79/comments","events_url":"https://api.github.com/repos/coq/coq/issues/79/events","html_url":"https://github.com/coq/coq/pull/79","id":90904493,"number":79,"title":"Let the kernel assume that a (co-)inductive type is positive","user":{"login":"aspiwack","id":1413217,"avatar_url":"https://avatars.githubusercontent.com/u/1413217?v=3","gravatar_id":"","url":"https://api.github.com/users/aspiwack","html_url":"https://github.com/aspiwack","followers_url":"https://api.github.com/users/aspiwack/followers","following_url":"https://api.github.com/users/aspiwack/following{/other_user}","gists_url":"https://api.github.com/users/aspiwack/gists{/gist_id}","starred_url":"https://api.github.com/users/aspiwack/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/aspiwack/subscriptions","organizations_url":"https://api.github.com/users/aspiwack/orgs","repos_url":"https://api.github.com/users/aspiwack/repos","events_url":"https://api.github.com/users/aspiwack/events{/privacy}","received_events_url":"https://api.github.com/users/aspiwack/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":8,"created_at":"2015-06-25T09:14:31Z","updated_at":"2015-07-03T12:18:44Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/79","html_url":"https://github.com/coq/coq/pull/79","diff_url":"https://github.com/coq/coq/pull/79.diff","patch_url":"https://github.com/coq/coq/pull/79.patch"},"body":"For the sake of experimentation, or just because it is an assumption no different in essence from an `Axiom`, it is useful to use a type that Coq does not recognise as positive.\r\n\r\nThe syntax I chose for this was `Assume [Positive] Inductive`. Another possibility may be `Assuming [Positive] Inductive`. The square bracket delimit a list, because of potential future things that could be assumed (also in Definitions) like `Assume [Guarded]` or `Assume [Guarded Wellsized]` (to ignore guard conditions and universe inconsistencies).\r\n\r\nHere is a view of coqide with this feature:\r\n\r\n![assumepositive](https://cloud.githubusercontent.com/assets/1413217/8351073/d1eebe36-1b2a-11e5-9151-cf650a5b2137.png)\r\n\r\nDoes anyone want to review the (minimal) changes to the kernel? (I'm fairly confident about them, I believe the test-suite thingies that I added to have a good coverage). Any advice or comment on the syntax?"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/118332998","html_url":"https://github.com/coq/coq/pull/79#issuecomment-118332998","issue_url":"https://api.github.com/repos/coq/coq/issues/79","id":118332998,"user":{"login":"herbelin","id":460771,"avatar_url":"https://avatars.githubusercontent.com/u/460771?v=3","gravatar_id":"","url":"https://api.github.com/users/herbelin","html_url":"https://github.com/herbelin","followers_url":"https://api.github.com/users/herbelin/followers","following_url":"https://api.github.com/users/herbelin/following{/other_user}","gists_url":"https://api.github.com/users/herbelin/gists{/gist_id}","starred_url":"https://api.github.com/users/herbelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/herbelin/subscriptions","organizations_url":"https://api.github.com/users/herbelin/orgs","repos_url":"https://api.github.com/users/herbelin/repos","events_url":"https://api.github.com/users/herbelin/events{/privacy}","received_events_url":"https://api.github.com/users/herbelin/received_events","type":"User","site_admin":false},"created_at":"2015-07-03T12:18:44Z","updated_at":"2015-07-03T12:18:44Z","body":"I propose that the ability to deactivate Guarded-ness, and Wellsized-ness is first implemented. Then we discuss about a user syntax for it.\r\n"}}