{"action":"closed","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3476","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3476/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3476/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3476/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3476","id":180992254,"number":3476,"title":"%runElab deriveElim produces \"No such variable Pruviloj.Core.Infer\"","user":{"login":"enolan","id":61517,"avatar_url":"https://avatars.githubusercontent.com/u/61517?v=3","gravatar_id":"","url":"https://api.github.com/users/enolan","html_url":"https://github.com/enolan","followers_url":"https://api.github.com/users/enolan/followers","following_url":"https://api.github.com/users/enolan/following{/other_user}","gists_url":"https://api.github.com/users/enolan/gists{/gist_id}","starred_url":"https://api.github.com/users/enolan/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/enolan/subscriptions","organizations_url":"https://api.github.com/users/enolan/orgs","repos_url":"https://api.github.com/users/enolan/repos","events_url":"https://api.github.com/users/enolan/events{/privacy}","received_events_url":"https://api.github.com/users/enolan/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2016-10-04T20:10:30Z","updated_at":"2016-10-06T15:30:55Z","closed_at":"2016-10-06T15:30:55Z","body":"This file:\r\n```idris\r\nimport Pruviloj.Derive.Eliminators\r\n\r\n%runElab deriveElim `{{Bool}} `{{boolelim}}\r\n```\r\nGives the error:\r\n```\r\n     ____    __     _                                          \r\n    /  _/___/ /____(_)____                                     \r\n    / // __  / ___/ / ___/     Version 0.12.3-git:59287a7\r\n  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      \r\n /___/\\__,_/_/  /_/____/       Type :? for help               \r\n\r\nIdris is free software with ABSOLUTELY NO WARRANTY.            \r\nFor details type :warranty.\r\nType checking ./derivebug.idr\r\nderivebug.idr:3:1-9:While running an elaboration script, the following error occurred:\r\nNo such variable Pruviloj.Core.Infer\r\n```\r\n\r\nIt works if I add `import Pruviloj.Core` to the top of the file. Apostolis and Melvar on IRC said this has happened before and the cause was module names being incorrect in the library."}}
{"actor":{"display_login":"david-christiansen"}}