{"action":"opened","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3890","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3890/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3890/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3890/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/3890","id":239049555,"number":3890,"title":"The implementation of Foldable (Vect n).","user":{"login":"Junology","id":1933073,"avatar_url":"https://avatars0.githubusercontent.com/u/1933073?v=3","gravatar_id":"","url":"https://api.github.com/users/Junology","html_url":"https://github.com/Junology","followers_url":"https://api.github.com/users/Junology/followers","following_url":"https://api.github.com/users/Junology/following{/other_user}","gists_url":"https://api.github.com/users/Junology/gists{/gist_id}","starred_url":"https://api.github.com/users/Junology/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Junology/subscriptions","organizations_url":"https://api.github.com/users/Junology/orgs","repos_url":"https://api.github.com/users/Junology/repos","events_url":"https://api.github.com/users/Junology/events{/privacy}","received_events_url":"https://api.github.com/users/Junology/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-06-28T04:26:53Z","updated_at":"2017-06-28T04:26:53Z","closed_at":null,"body":"Please tell me why Foldable (Vect n) has such a complicated implementation:\r\n```idris\r\nfoldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc\r\nfoldrImpl f e go [] = go e\r\nfoldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs\r\n\r\nimplementation Foldable (Vect n) where\r\nfoldr f e xs = foldrImpl f e id xs\r\n```\r\nI am asking this question because I need to have a proof of the following type.\r\n```idris\r\nprop_sum : {x : Nat} -> {xs : Vect n Nat} -> sum (x::xs) = x + sum xs\r\n```\r\nThis _obvious_ proposition is not actually obvious with ``Foldable (Vect n)`` above.\r\nNote it is obvious for ``List`` since it has a straightforward implementation of ``Foldable``."}}
{"actor":{"display_login":"Junology"}}