{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3481","repository_url":"https://api.github.com/repos/idris-lang/Idris-dev","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3481/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3481/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3481/events","html_url":"https://github.com/idris-lang/Idris-dev/pull/3481","id":181887466,"number":3481,"title":"Print interface parameter constraints in :doc","user":{"login":"owickstrom","id":1464328,"avatar_url":"https://avatars.githubusercontent.com/u/1464328?v=3","gravatar_id":"","url":"https://api.github.com/users/owickstrom","html_url":"https://github.com/owickstrom","followers_url":"https://api.github.com/users/owickstrom/followers","following_url":"https://api.github.com/users/owickstrom/following{/other_user}","gists_url":"https://api.github.com/users/owickstrom/gists{/gist_id}","starred_url":"https://api.github.com/users/owickstrom/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/owickstrom/subscriptions","organizations_url":"https://api.github.com/users/owickstrom/orgs","repos_url":"https://api.github.com/users/owickstrom/repos","events_url":"https://api.github.com/users/owickstrom/events{/privacy}","received_events_url":"https://api.github.com/users/owickstrom/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":9,"created_at":"2016-10-09T13:41:27Z","updated_at":"2016-10-17T00:49:19Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/pulls/3481","html_url":"https://github.com/idris-lang/Idris-dev/pull/3481","diff_url":"https://github.com/idris-lang/Idris-dev/pull/3481.diff","patch_url":"https://github.com/idris-lang/Idris-dev/pull/3481.patch"},"body":"This should fix #3157.\r\n\r\n**Things to note:**\r\n\r\n* I've changed so constraints are passed along as `[PTerm]` from `PInterface`, through   \r\n  `CI` (`InterfaceInfo` constructor), to `InterfaceDoc`. Not sure `PTerm` is preferable, what do you think?\r\n* The constraints are printed before the parameters on a single line, if the parameters are printed on a single line.\r\n* If the parameters are printed on multiple lines, the constraints are printed on a separate single line above the parameters.\r\n\r\n**Examples (abbr.)**\r\n\r\nThe `Ord` interface:\r\n\r\n```\r\nIdris> :doc Ord\r\nInterface Ord\r\n    The Ord interface defines comparison operations on ordered data types.\r\n\r\nParameters:\r\n    Eq ty => ty\r\n\r\nMethods:\r\n    ...\r\n```\r\n\r\nAnd :doc on an interface with multiple documented parameters:\r\n\r\n```\r\n$ cat ../Interfaces.idr\r\n||| The Cool interface\r\n||| @ a A parameter.\r\n||| @ b Another parameter.\r\ninterface (Eq a, Num a, Ord b) => Cool a b\r\nwhere\r\n  isCool  : (a, b) -> Bool\r\n$ idris -- ../Interfaces.idr\r\n*../Interfaces> :doc Cool\r\nInterface Cool\r\n    The Cool interface\r\n\r\nParameters:\r\n    (Eq a, Num a, Ord b) =>\r\n    a   -- A parameter.\r\n    b   -- Another parameter.\r\n\r\nMethods:\r\n    ...\r\n```"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/254089486","html_url":"https://github.com/idris-lang/Idris-dev/pull/3481#issuecomment-254089486","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/3481","id":254089486,"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-10-17T00:49:18Z","updated_at":"2016-10-17T00:49:18Z","body":"I don't think so, but I'll give it a peek from my work computer tomorrow.\nThanks for this!\n\n2016-10-16 2:50 GMT-04:00 Oskar Wickström <notifications@github.com>:\n\n> Ping 😀 anything more that needs to be done?\n>\n> —\n> You are receiving this because you commented.\n> Reply to this email directly, view it on GitHub\n> <https://github.com/idris-lang/Idris-dev/pull/3481#issuecomment-254030897>,\n> or mute the thread\n> <https://github.com/notifications/unsubscribe-auth/AAHCgjwK0UQ8BHLlGvVIXHOgZVtpnRIyks5q0ck7gaJpZM4KSAMS>\n> .\n>\n"}}
{"actor":{"display_login":"david-christiansen"}}