{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1983","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1983/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1983/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1983/events","html_url":"https://github.com/idris-lang/Idris-dev/pull/1983","id":60174420,"number":1983,"title":"Instance docs","user":{"login":"adamse","id":75746,"avatar_url":"https://avatars.githubusercontent.com/u/75746?v=3","gravatar_id":"","url":"https://api.github.com/users/adamse","html_url":"https://github.com/adamse","followers_url":"https://api.github.com/users/adamse/followers","following_url":"https://api.github.com/users/adamse/following{/other_user}","gists_url":"https://api.github.com/users/adamse/gists{/gist_id}","starred_url":"https://api.github.com/users/adamse/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/adamse/subscriptions","organizations_url":"https://api.github.com/users/adamse/orgs","repos_url":"https://api.github.com/users/adamse/repos","events_url":"https://api.github.com/users/adamse/events{/privacy}","received_events_url":"https://api.github.com/users/adamse/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-03-06T23:30:15Z","updated_at":"2015-03-07T12:10:47Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/pulls/1983","html_url":"https://github.com/idris-lang/Idris-dev/pull/1983","diff_url":"https://github.com/idris-lang/Idris-dev/pull/1983.diff","patch_url":"https://github.com/idris-lang/Idris-dev/pull/1983.patch"},"body":"Implementation of instance docs as proposed in #1943.\r\n\r\nThis is not quite finished, here are some items to do:\r\n\r\n- [x] Update types & plumb types\r\n- [x] Parse instance docs\r\n    - [ ] Refactor parser to remove added `try`s?\r\n- [x] Add `Docstring` to compiler state\r\n- [ ] Tests\r\n- [x] Show instance docs in `:doc`\r\n- [ ] Show instance docs in html\r\n- [ ] Update documentation where applicable\r\n\r\nExample\r\n~~~\r\n> echo \":doc Functor\" | ./dist/build/Idris/idris ./libs/prelude/Prelude/Functor.idr\r\n[...]\r\nInstances:\r\n    Functor id\r\n      The id-entity functor\r\n    Functor List\r\n[...]\r\n~~~\r\nwith\r\n~~~idris\r\n||| The id-entity functor\r\ninstance Functor id where\r\n    map f a = f a\r\n~~~\r\nin `Prelude.Functor`."},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/77686779","html_url":"https://github.com/idris-lang/Idris-dev/pull/1983#issuecomment-77686779","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/1983","id":77686779,"user":{"login":"adamse","id":75746,"avatar_url":"https://avatars.githubusercontent.com/u/75746?v=3","gravatar_id":"","url":"https://api.github.com/users/adamse","html_url":"https://github.com/adamse","followers_url":"https://api.github.com/users/adamse/followers","following_url":"https://api.github.com/users/adamse/following{/other_user}","gists_url":"https://api.github.com/users/adamse/gists{/gist_id}","starred_url":"https://api.github.com/users/adamse/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/adamse/subscriptions","organizations_url":"https://api.github.com/users/adamse/orgs","repos_url":"https://api.github.com/users/adamse/repos","events_url":"https://api.github.com/users/adamse/events{/privacy}","received_events_url":"https://api.github.com/users/adamse/received_events","type":"User","site_admin":false},"created_at":"2015-03-07T12:10:47Z","updated_at":"2015-03-07T12:10:47Z","body":"I like the idea of a \"documentable declaration\" parser as it would reduce code duplication. But wouldn't it include type declarations, data declarations, postulates, records and functions as well?"}}