{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2639","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2639/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2639/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2639/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2639","id":107381574,"number":2639,"title":"Safe String to Int function.","user":{"login":"NightRa","id":2140983,"avatar_url":"https://avatars.githubusercontent.com/u/2140983?v=3","gravatar_id":"","url":"https://api.github.com/users/NightRa","html_url":"https://github.com/NightRa","followers_url":"https://api.github.com/users/NightRa/followers","following_url":"https://api.github.com/users/NightRa/following{/other_user}","gists_url":"https://api.github.com/users/NightRa/gists{/gist_id}","starred_url":"https://api.github.com/users/NightRa/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/NightRa/subscriptions","organizations_url":"https://api.github.com/users/NightRa/orgs","repos_url":"https://api.github.com/users/NightRa/repos","events_url":"https://api.github.com/users/NightRa/events{/privacy}","received_events_url":"https://api.github.com/users/NightRa/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/Feature%20request","name":"Feature request","color":"207de5"},{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/Low%20hanging%20fruit","name":"Low hanging fruit","color":"5319e7"},{"url":"https://api.github.com/repos/idris-lang/Idris-dev/labels/Patches%20welcome!","name":"Patches welcome!","color":"207de5"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":10,"created_at":"2015-09-20T09:23:40Z","updated_at":"2015-09-30T08:53:05Z","closed_at":null,"body":"There should definitely be a safe function for parsing Ints from Strings in the standard library.\r\n```idris\r\nparseInt : String -> Maybe Int\r\n```\r\n\r\nThe existance of an unchecked Cast from String to Int in Idris is really bewildering to me, and in my opinion, it shouldn't even exist.\r\n\r\n```idris\r\nx : Int\r\nx = cast \"hello\"\r\n> x = 0\r\n```"},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/144331036","html_url":"https://github.com/idris-lang/Idris-dev/issues/2639#issuecomment-144331036","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2639","id":144331036,"user":{"login":"eklavya","id":1136647,"avatar_url":"https://avatars.githubusercontent.com/u/1136647?v=3","gravatar_id":"","url":"https://api.github.com/users/eklavya","html_url":"https://github.com/eklavya","followers_url":"https://api.github.com/users/eklavya/followers","following_url":"https://api.github.com/users/eklavya/following{/other_user}","gists_url":"https://api.github.com/users/eklavya/gists{/gist_id}","starred_url":"https://api.github.com/users/eklavya/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/eklavya/subscriptions","organizations_url":"https://api.github.com/users/eklavya/orgs","repos_url":"https://api.github.com/users/eklavya/repos","events_url":"https://api.github.com/users/eklavya/events{/privacy}","received_events_url":"https://api.github.com/users/eklavya/received_events","type":"User","site_admin":false},"created_at":"2015-09-30T08:53:05Z","updated_at":"2015-09-30T08:53:05Z","body":"Hi,\r\n\r\nWould this do?\r\n```Idris\r\nparseInt : String -> Maybe Int                                                                                                                                                       \r\nparseInt \"\"             | StrNil = Nothing                                                                                                                                           \r\nparseInt s                       = parseIntAux (unpack s) 0 where                                                                                                                    \r\n    parseIntAux : (List Char) -> Int -> Maybe Int                                                                                                                                    \r\n    parseIntAux [] acc             = Just acc                                                                                                                                        \r\n    parseIntAux (c :: cs) acc = if (c >= '0' && c <= '9') then parseIntAux cs ((acc * 10) + (ord c) - 48)                                                                            \r\n                                                          else Nothing \r\n```\r\n\r\nI am a newbie, so I thought I'd ask before creating a PR or anything."}}