{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1767","labels_url":"https://api.github.com/repos/agda/agda/issues/1767/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1767/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1767/events","html_url":"https://github.com/agda/agda/issues/1767","id":125416505,"number":1767,"title":"Positivity check: Renaming options and pragmas","user":{"login":"asr","id":635804,"avatar_url":"https://avatars.githubusercontent.com/u/635804?v=3","gravatar_id":"","url":"https://api.github.com/users/asr","html_url":"https://github.com/asr","followers_url":"https://api.github.com/users/asr/followers","following_url":"https://api.github.com/users/asr/following{/other_user}","gists_url":"https://api.github.com/users/asr/gists{/gist_id}","starred_url":"https://api.github.com/users/asr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/asr/subscriptions","organizations_url":"https://api.github.com/users/asr/orgs","repos_url":"https://api.github.com/users/asr/repos","events_url":"https://api.github.com/users/asr/events{/privacy}","received_events_url":"https://api.github.com/users/asr/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/info-needed","name":"info-needed","color":"159818"},{"url":"https://api.github.com/repos/agda/agda/labels/positivity","name":"positivity","color":"ededed"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-01-07T15:33:28Z","updated_at":"2016-01-08T05:00:28Z","closed_at":"2016-01-08T05:00:28Z","body":"I want to make the following renaming:\r\n\r\n`--no-positivity-check` -> `--no-strict-positivity-check` (in master)\r\n\r\n`NO_POSITIVITY_CHECK` -> `NO_STRICT_POSITIVITY_CHECK` (in master and maint-2.4)\r\n\r\nMotivation: I would like to add an option for experimenting with positive but not-strictly positive types in the future.\r\n\r\nAny objection?\r\n"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/169897294","html_url":"https://github.com/agda/agda/issues/1767#issuecomment-169897294","issue_url":"https://api.github.com/repos/agda/agda/issues/1767","id":169897294,"user":{"login":"asr","id":635804,"avatar_url":"https://avatars.githubusercontent.com/u/635804?v=3","gravatar_id":"","url":"https://api.github.com/users/asr","html_url":"https://github.com/asr","followers_url":"https://api.github.com/users/asr/followers","following_url":"https://api.github.com/users/asr/following{/other_user}","gists_url":"https://api.github.com/users/asr/gists{/gist_id}","starred_url":"https://api.github.com/users/asr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/asr/subscriptions","organizations_url":"https://api.github.com/users/asr/orgs","repos_url":"https://api.github.com/users/asr/repos","events_url":"https://api.github.com/users/asr/events{/privacy}","received_events_url":"https://api.github.com/users/asr/received_events","type":"User","site_admin":false},"created_at":"2016-01-08T05:00:28Z","updated_at":"2016-01-08T05:00:28Z","body":"> Also, I think NO_POSITIVITY_CHECK is already on the long side and should not get longer. One could think of a shorter pragma STRICTLY_POSITIVE, analogously to TERMINATING.\r\n\r\nI agree with the shorter pragma."}}