{"action":"opened","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3889","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3889/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3889/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3889/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3889","id":238910808,"number":3889,"title":"INTERNAL ERROR when creating ElabReflection-produced definition twice in the REPL","user":{"login":"RyanGlScott","id":2364661,"avatar_url":"https://avatars1.githubusercontent.com/u/2364661?v=3","gravatar_id":"","url":"https://api.github.com/users/RyanGlScott","html_url":"https://github.com/RyanGlScott","followers_url":"https://api.github.com/users/RyanGlScott/followers","following_url":"https://api.github.com/users/RyanGlScott/following{/other_user}","gists_url":"https://api.github.com/users/RyanGlScott/gists{/gist_id}","starred_url":"https://api.github.com/users/RyanGlScott/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RyanGlScott/subscriptions","organizations_url":"https://api.github.com/users/RyanGlScott/orgs","repos_url":"https://api.github.com/users/RyanGlScott/repos","events_url":"https://api.github.com/users/RyanGlScott/events{/privacy}","received_events_url":"https://api.github.com/users/RyanGlScott/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-06-27T16:32:23Z","updated_at":"2017-06-27T16:32:23Z","closed_at":null,"body":"```\r\n$ idris -p pruviloj -XElabReflection\r\n     ____    __     _                                          \r\n    /  _/___/ /____(_)____                                     \r\n    / // __  / ___/ / ___/     Version 1.0\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\nIdris> :module Pruviloj.Derive.Eliminators\r\n*Pruviloj/Derive/Eliminators> :let %runElab (deriveElim `{{List}} `{{elimList}})\r\n*Pruviloj/Derive/Eliminators> :let %runElab (deriveElim `{{List}} `{{elimList}})\r\n(input):1:6-14:While running an elaboration script, the following error occurred:\r\nINTERNAL ERROR: elimList is already defined.\r\nThis is probably a bug, or a missing error message.\r\nPlease consider reporting at https://github.com/idris-lang/Idris-dev/issues\r\n```"}}
{"actor":{"display_login":"RyanGlScott"}}