{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2368","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2368/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2368/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2368/events","html_url":"https://github.com/agda/agda/issues/2368","id":198078877,"number":2368,"title":"Internal error after refining a tactic @ MetaVars.hs:267","user":{"login":"m0davis","id":203587,"avatar_url":"https://avatars.githubusercontent.com/u/203587?v=3","gravatar_id":"","url":"https://api.github.com/users/m0davis","html_url":"https://github.com/m0davis","followers_url":"https://api.github.com/users/m0davis/followers","following_url":"https://api.github.com/users/m0davis/following{/other_user}","gists_url":"https://api.github.com/users/m0davis/gists{/gist_id}","starred_url":"https://api.github.com/users/m0davis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/m0davis/subscriptions","organizations_url":"https://api.github.com/users/m0davis/orgs","repos_url":"https://api.github.com/users/m0davis/repos","events_url":"https://api.github.com/users/m0davis/events{/privacy}","received_events_url":"https://api.github.com/users/m0davis/received_events","type":"User","site_admin":false},"labels":[{"id":245647317,"url":"https://api.github.com/repos/agda/agda/labels/bug","name":"bug","color":"fc2929","default":true},{"id":245649251,"url":"https://api.github.com/repos/agda/agda/labels/interaction","name":"interaction","color":"ededed","default":false},{"id":245647680,"url":"https://api.github.com/repos/agda/agda/labels/meta","name":"meta","color":"ededed","default":false},{"id":245648655,"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":4,"created_at":"2016-12-29T22:34:57Z","updated_at":"2016-12-30T14:50:53Z","closed_at":null,"body":"This one seemed a bit too daunting for me to simplify. It uses agda-prelude.\r\n```\r\nopen import Tactic.Nat\r\nopen import Prelude.Nat\r\nopen import Prelude.Empty\r\nopen import Prelude.Bool\r\nopen import Prelude.Equality\r\n\r\nlemma : ∀ {m n : Nat} → ¬ IsTrue (lessNat m n) → ¬ IsTrue (lessNat n m) → m ≡ n\r\nlemma {zero} {zero} m≮n n≮m = refl\r\nlemma {zero} {suc n} m≮n n≮m = ⊥-elim (m≮n true)\r\nlemma {suc m} {zero} m≮n n≮m = ⊥-elim (n≮m true)\r\nlemma {suc m} {suc n} m≮n n≮m = by (lemma {m} {n} {!m≮n!} {!n≮m!})\r\n```\r\nRefine (C-c C-r) the hole containing `m≮n`, then refine (without reloading) the last hole. The result is:\r\n```\r\nAn internal error has occurred. Please report this as a bug.\r\nLocation of the error: src/full/Agda/TypeChecking/Monad/MetaVars.hs:267\r\n```"},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/269779749","html_url":"https://github.com/agda/agda/issues/2368#issuecomment-269779749","issue_url":"https://api.github.com/repos/agda/agda/issues/2368","id":269779749,"user":{"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},"created_at":"2016-12-30T14:50:53Z","updated_at":"2016-12-30T14:50:53Z","body":"A solution would be to never remove interaction points from the store, rather just mark them as solved."}}
{"actor":{"display_login":"andreasabel"}}