{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/480","repository_url":"https://api.github.com/repos/UniMath/UniMath","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/480/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/480/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/480/events","html_url":"https://github.com/UniMath/UniMath/issues/480","id":184843782,"number":480,"title":"Aborted proofs in UniMath","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},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2016-10-24T13:41:42Z","updated_at":"2016-10-25T18:12:34Z","closed_at":null,"body":"Thanks to a question by Tomi I discovered that there are aborted proofs in FiniteSequences.\r\n\r\nThis raises three issues:\r\n\r\n1. Please, in the future immediately let everybody know if you find aborted or admitted proofs. Such \"proofs\" are strictly forbidden in the UniMath.\r\n\r\n2. Please immediately remove all statements without full proofs or complete the proofs as the very first priority. \r\n\r\n3. Please (@DanGdayson, @JasonGross?) write a script that will be run every time the make is run that will check that the words \"abort\" and \"admit\" do not occur in the .v files.  "},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/256115666","html_url":"https://github.com/UniMath/UniMath/issues/480#issuecomment-256115666","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/480","id":256115666,"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-10-25T18:12:34Z","updated_at":"2016-10-25T18:12:34Z","body":"There is a reason. UniMath is a library that should be clean. Aborted proofs are Ok in individual forks but there is no reason to have an aborted proof in the library.\n\n> On Oct 24, 2016, at 7:04 PM, Daniel R. Grayson <notifications@github.com> wrote:\n> \n> We don't have a rule against aborted proofs, only against admitted proofs. And there\n> is no reason to introduce such a rule, since an aborted proof results in no definitions.\n> \n> —\n> You are receiving this because you authored the thread.\n> Reply to this email directly, view it on GitHub <https://github.com/UniMath/UniMath/issues/480#issuecomment-255890666>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAZ4S8yTBqTAyOz9jM0b4YBPzyuS52Rzks5q3TlqgaJpZM4KezVK>.\n> \n\n"}}
{"actor":{"display_login":"vladimirias"}}