{"action":"opened","issue":{"url":"https://api.github.com/repos/agda/agda/issues/3467","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/3467/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/3467/comments","events_url":"https://api.github.com/repos/agda/agda/issues/3467/events","html_url":"https://github.com/agda/agda/issues/3467","id":393525055,"node_id":"MDU6SXNzdWUzOTM1MjUwNTU=","number":3467,"title":"unquoteDef/unquoteDecl does not accept where-blocks","user":{"login":"guillaumebrunerie","id":787865,"node_id":"MDQ6VXNlcjc4Nzg2NQ==","avatar_url":"https://avatars1.githubusercontent.com/u/787865?v=4","gravatar_id":"","url":"https://api.github.com/users/guillaumebrunerie","html_url":"https://github.com/guillaumebrunerie","followers_url":"https://api.github.com/users/guillaumebrunerie/followers","following_url":"https://api.github.com/users/guillaumebrunerie/following{/other_user}","gists_url":"https://api.github.com/users/guillaumebrunerie/gists{/gist_id}","starred_url":"https://api.github.com/users/guillaumebrunerie/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/guillaumebrunerie/subscriptions","organizations_url":"https://api.github.com/users/guillaumebrunerie/orgs","repos_url":"https://api.github.com/users/guillaumebrunerie/repos","events_url":"https://api.github.com/users/guillaumebrunerie/events{/privacy}","received_events_url":"https://api.github.com/users/guillaumebrunerie/received_events","type":"User","site_admin":false},"labels":[{"id":245648655,"node_id":"MDU6TGFiZWwyNDU2NDg2NTU=","url":"https://api.github.com/repos/agda/agda/labels/reflection","name":"reflection","color":"ededed","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-12-21T16:54:48Z","updated_at":"2018-12-21T16:54:48Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"Is there a reason why one cannot add where-blocks to `unquoteDef`/`unquoteDecl`?\r\n\r\n```agda\r\nunquoteDecl a = ? where\r\n  b = ?\r\n```\r\ngives a parse error at the `where`."}}
{"actor":{"display_login":"guillaumebrunerie"}}