{"action":"created","issue":{"url":"https://api.github.com/repos/banacorn/agda-mode/issues/51","repository_url":"https://api.github.com/repos/banacorn/agda-mode","labels_url":"https://api.github.com/repos/banacorn/agda-mode/issues/51/labels{/name}","comments_url":"https://api.github.com/repos/banacorn/agda-mode/issues/51/comments","events_url":"https://api.github.com/repos/banacorn/agda-mode/issues/51/events","html_url":"https://github.com/banacorn/agda-mode/issues/51","id":262353980,"number":51,"title":"Type error on hole-related operations","user":{"login":"aochagavia","id":5196584,"avatar_url":"https://avatars1.githubusercontent.com/u/5196584?v=4","gravatar_id":"","url":"https://api.github.com/users/aochagavia","html_url":"https://github.com/aochagavia","followers_url":"https://api.github.com/users/aochagavia/followers","following_url":"https://api.github.com/users/aochagavia/following{/other_user}","gists_url":"https://api.github.com/users/aochagavia/gists{/gist_id}","starred_url":"https://api.github.com/users/aochagavia/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/aochagavia/subscriptions","organizations_url":"https://api.github.com/users/aochagavia/orgs","repos_url":"https://api.github.com/users/aochagavia/repos","events_url":"https://api.github.com/users/aochagavia/events{/privacy}","received_events_url":"https://api.github.com/users/aochagavia/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":7,"created_at":"2017-10-03T09:05:11Z","updated_at":"2017-10-13T13:08:27Z","closed_at":null,"author_association":"NONE","body":"## Version information\r\n\r\nOS: Windows 10 x64\r\nAtom: 1.20.1\r\nElectron: 1.6.9\r\nChrome: 56.0.2924.87\r\nNode: 7.4.0\r\nagda-mode: 0.7.2\r\nlanguage-agda: 0.2.5\r\n\r\n## Problem\r\n\r\nWhen using holes, the refine (`C-c C-r`) and auto (`C-c C-a`) commands don't work. Both result in a TypeError from Atom: `Cannot read property 'core' of undefined`. This seems to be an internal error of the `agda-mode` package.\r\n\r\nOther commands like `C-c C-l` are working all right.\r\n\r\n## How to trigger the error\r\n\r\nUse the following program and try \r\n\r\n```agda\r\nmodule test where\r\n\r\n-- Prelude --\r\n\r\ndata Nat : Set where\r\n  Zero : Nat\r\n  Succ : Nat -> Nat\r\n\r\ndata _==_ {a : Set} (x : a) : a -> Set where\r\n  Refl : x == x\r\n\r\ncong : {a b : Set} {x y : a} -> (f : a -> b) -> x == y -> f x  == f y\r\ncong f Refl = Refl\r\n\r\ntrans : {a : Set} {x y z : a} -> x == y -> y == z -> x == z\r\ntrans Refl q = q\r\n\r\nsym : {a : Set} {x y : a} -> x == y -> y == x\r\nsym Refl = Refl\r\n\r\n-- Examples\r\ntestEq : {x y : Nat} -> x == y -> Succ x == Succ y\r\ntestEq proof = cong Succ ?\r\n```\r\n\r\nIt is clear that the hole in `testEq` should be filled with `proof`. However, even after entering the text `proof`, an attempt to refine results in the error I describe above.\r\n\r\n## Stack trace\r\n\r\nI would like to include a stack trace, but I don't know how to get a stack trace from Atom, so sorry for that."},"comment":{"url":"https://api.github.com/repos/banacorn/agda-mode/issues/comments/336447595","html_url":"https://github.com/banacorn/agda-mode/issues/51#issuecomment-336447595","issue_url":"https://api.github.com/repos/banacorn/agda-mode/issues/51","id":336447595,"user":{"login":"banacorn","id":797844,"avatar_url":"https://avatars1.githubusercontent.com/u/797844?v=4","gravatar_id":"","url":"https://api.github.com/users/banacorn","html_url":"https://github.com/banacorn","followers_url":"https://api.github.com/users/banacorn/followers","following_url":"https://api.github.com/users/banacorn/following{/other_user}","gists_url":"https://api.github.com/users/banacorn/gists{/gist_id}","starred_url":"https://api.github.com/users/banacorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/banacorn/subscriptions","organizations_url":"https://api.github.com/users/banacorn/orgs","repos_url":"https://api.github.com/users/banacorn/repos","events_url":"https://api.github.com/users/banacorn/events{/privacy}","received_events_url":"https://api.github.com/users/banacorn/received_events","type":"User","site_admin":false},"created_at":"2017-10-13T13:08:27Z","updated_at":"2017-10-13T13:08:27Z","author_association":"OWNER","body":"Hmm ... this is weird because agda-mode should be sending \r\n```... (intervalsToRange (Just (mkAbsolute ...``` \r\ninstead of \r\n```... (Range [Interval (Pn (Just (mkAbsolute ...```\r\nafter v2.5.1"}}
{"actor":{"display_login":"banacorn"}}