{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1986","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/1986/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1986/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1986/events","html_url":"https://github.com/agda/agda/issues/1986","id":155672008,"number":1986,"title":"Compilation of copattern matching with catch-all","user":{"login":"nad","id":293222,"avatar_url":"https://avatars.githubusercontent.com/u/293222?v=3","gravatar_id":"","url":"https://api.github.com/users/nad","html_url":"https://github.com/nad","followers_url":"https://api.github.com/users/nad/followers","following_url":"https://api.github.com/users/nad/following{/other_user}","gists_url":"https://api.github.com/users/nad/gists{/gist_id}","starred_url":"https://api.github.com/users/nad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nad/subscriptions","organizations_url":"https://api.github.com/users/nad/orgs","repos_url":"https://api.github.com/users/nad/repos","events_url":"https://api.github.com/users/nad/events{/privacy}","received_events_url":"https://api.github.com/users/nad/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/compiler-treeless","name":"compiler-treeless","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/copatterns","name":"copatterns","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/pattern-matching","name":"pattern-matching","color":"ededed"},{"url":"https://api.github.com/repos/agda/agda/labels/priority-high","name":"priority-high","color":"ededed"}],"state":"open","locked":false,"assignee":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/16","html_url":"https://github.com/agda/agda/milestones/2.5.2","labels_url":"https://api.github.com/repos/agda/agda/milestones/16/labels","id":1713715,"number":16,"title":"2.5.2","description":null,"creator":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"open_issues":21,"closed_issues":34,"state":"open","created_at":"2016-04-18T13:25:09Z","updated_at":"2016-06-02T14:13:02Z","due_on":null,"closed_at":null},"comments":6,"created_at":"2016-05-19T07:37:03Z","updated_at":"2016-06-02T21:50:33Z","closed_at":null,"body":"Consider the following code:\r\n```agda\r\ndata Bool : Set where\r\n  true false : Bool\r\n\r\nf : Bool → Set₁\r\nf true = Set\r\nf      = λ _ → Set\r\n```\r\nAgda fails to see that the pattern matching in `f` is complete:\r\n```\r\nIncomplete pattern matching for f. Missing cases:\r\n  f false\r\nwhen checking the definition of f\r\n```\r\nIs this intended?"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/223433646","html_url":"https://github.com/agda/agda/issues/1986#issuecomment-223433646","issue_url":"https://api.github.com/repos/agda/agda/issues/1986","id":223433646,"user":{"login":"phile314","id":1640697,"avatar_url":"https://avatars.githubusercontent.com/u/1640697?v=3","gravatar_id":"","url":"https://api.github.com/users/phile314","html_url":"https://github.com/phile314","followers_url":"https://api.github.com/users/phile314/followers","following_url":"https://api.github.com/users/phile314/following{/other_user}","gists_url":"https://api.github.com/users/phile314/gists{/gist_id}","starred_url":"https://api.github.com/users/phile314/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/phile314/subscriptions","organizations_url":"https://api.github.com/users/phile314/orgs","repos_url":"https://api.github.com/users/phile314/repos","events_url":"https://api.github.com/users/phile314/events{/privacy}","received_events_url":"https://api.github.com/users/phile314/received_events","type":"User","site_admin":false},"created_at":"2016-06-02T21:50:33Z","updated_at":"2016-06-02T21:50:33Z","body":"I can give it a go in the next few days."}}
{"actor":{"display_login":"phile314"}}