{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3594","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3594/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3594/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3594/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3594","id":197905898,"number":3594,"title":"The Pruviloj.Induction.induction error message could be improved","user":{"login":"yurrriq","id":1866448,"avatar_url":"https://avatars.githubusercontent.com/u/1866448?v=3","gravatar_id":"","url":"https://api.github.com/users/yurrriq","html_url":"https://github.com/yurrriq","followers_url":"https://api.github.com/users/yurrriq/followers","following_url":"https://api.github.com/users/yurrriq/following{/other_user}","gists_url":"https://api.github.com/users/yurrriq/gists{/gist_id}","starred_url":"https://api.github.com/users/yurrriq/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/yurrriq/subscriptions","organizations_url":"https://api.github.com/users/yurrriq/orgs","repos_url":"https://api.github.com/users/yurrriq/repos","events_url":"https://api.github.com/users/yurrriq/events{/privacy}","received_events_url":"https://api.github.com/users/yurrriq/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":4,"created_at":"2016-12-28T19:42:55Z","updated_at":"2016-12-29T06:16:28Z","closed_at":"2016-12-29T06:01:01Z","body":"When I make this typo:\r\n\r\n```idris\r\nmapPreservesLen : (f : a -> b) -> (l : List a) ->\r\n                  length (map f l) = length l\r\nmapPreservesLen = %runElab mush\r\n```\r\n\r\n*[Specifically, I forgot to include `f` on the left-hand side.]*\r\n\r\nI get the [somewhat cryptic error message](https://github.com/idris-lang/Idris-dev/blob/v0.99/libs/pruviloj/Pruviloj/Induction.idr#L135):\r\n\r\n```\r\nWhen checking right hand side of mapPreservesLen with expected type\r\n        (f : a -> b) -> (l : List a) -> length (map f l) = length l\r\n\r\na -> b is not an inductive family\r\n```\r\n\r\n`f` needs to be on the left-hand side so we do induction on `l`, which, unlike `f`, **is** an *inductive family*:\r\n\r\n```idris\r\nmapPreservesLen f = %runElab mush\r\n```"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/269586890","html_url":"https://github.com/idris-lang/Idris-dev/issues/3594#issuecomment-269586890","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3594","id":269586890,"user":{"login":"david-christiansen","id":115330,"avatar_url":"https://avatars.githubusercontent.com/u/115330?v=3","gravatar_id":"","url":"https://api.github.com/users/david-christiansen","html_url":"https://github.com/david-christiansen","followers_url":"https://api.github.com/users/david-christiansen/followers","following_url":"https://api.github.com/users/david-christiansen/following{/other_user}","gists_url":"https://api.github.com/users/david-christiansen/gists{/gist_id}","starred_url":"https://api.github.com/users/david-christiansen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/david-christiansen/subscriptions","organizations_url":"https://api.github.com/users/david-christiansen/orgs","repos_url":"https://api.github.com/users/david-christiansen/repos","events_url":"https://api.github.com/users/david-christiansen/events{/privacy}","received_events_url":"https://api.github.com/users/david-christiansen/received_events","type":"User","site_admin":false},"created_at":"2016-12-29T06:16:28Z","updated_at":"2016-12-29T06:16:28Z","body":"Right, it's not highlighted because the highlighting is based on it having defined the function, and the function does not yet exist when it makes that message :-) It would be nice to figure out a model where that doesn't happen."}}
{"actor":{"display_login":"david-christiansen"}}