{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/2194","repository_url":"https://api.github.com/repos/agda/agda","labels_url":"https://api.github.com/repos/agda/agda/issues/2194/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/2194/comments","events_url":"https://api.github.com/repos/agda/agda/issues/2194/events","html_url":"https://github.com/agda/agda/issues/2194","id":177553862,"number":2194,"title":"JS backend returns `false` on `primFloatEquality NaN NaN`","user":{"login":"asr","id":635804,"avatar_url":"https://avatars.githubusercontent.com/u/635804?v=3","gravatar_id":"","url":"https://api.github.com/users/asr","html_url":"https://github.com/asr","followers_url":"https://api.github.com/users/asr/followers","following_url":"https://api.github.com/users/asr/following{/other_user}","gists_url":"https://api.github.com/users/asr/gists{/gist_id}","starred_url":"https://api.github.com/users/asr/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/asr/subscriptions","organizations_url":"https://api.github.com/users/asr/orgs","repos_url":"https://api.github.com/users/asr/repos","events_url":"https://api.github.com/users/asr/events{/privacy}","received_events_url":"https://api.github.com/users/asr/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/agda/agda/labels/bug","name":"bug","color":"fc2929"},{"url":"https://api.github.com/repos/agda/agda/labels/js-backend","name":"js-backend","color":"ededed"}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":{"url":"https://api.github.com/repos/agda/agda/milestones/16","html_url":"https://github.com/agda/agda/milestones/2.5.2","labels_url":"https://api.github.com/repos/agda/agda/milestones/16/labels","id":1713715,"number":16,"title":"2.5.2","description":null,"creator":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"open_issues":35,"closed_issues":134,"state":"open","created_at":"2016-04-18T13:25:09Z","updated_at":"2016-09-18T11:14:17Z","due_on":null,"closed_at":null},"comments":9,"created_at":"2016-09-17T03:52:40Z","updated_at":"2016-09-18T12:55:17Z","closed_at":null,"body":"```agda\r\nopen import Common.Prelude\r\n\r\nprintB : Bool → IO Unit\r\nprintB true  = putStrLn \"true\"\r\nprintB false = putStrLn \"false\"\r\n\r\n_/_ = primFloatDiv\r\n_==_ = primFloatEquality\r\n\r\nNaN : Float\r\nNaN = 0.0 / 0.0\r\n\r\nmain : IO Unit\r\nmain = printB (NaN == NaN)\r\n```\r\n\r\nOn the above code the backends return as follows:\r\n\r\nGHC: `true`\r\nUHC: `true`\r\nJS: `false`\r\n\r\nThe JS backend also should returns `true` (see #2155)."},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/247846136","html_url":"https://github.com/agda/agda/issues/2194#issuecomment-247846136","issue_url":"https://api.github.com/repos/agda/agda/issues/2194","id":247846136,"user":{"login":"andreasabel","id":1155218,"avatar_url":"https://avatars.githubusercontent.com/u/1155218?v=3","gravatar_id":"","url":"https://api.github.com/users/andreasabel","html_url":"https://github.com/andreasabel","followers_url":"https://api.github.com/users/andreasabel/followers","following_url":"https://api.github.com/users/andreasabel/following{/other_user}","gists_url":"https://api.github.com/users/andreasabel/gists{/gist_id}","starred_url":"https://api.github.com/users/andreasabel/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andreasabel/subscriptions","organizations_url":"https://api.github.com/users/andreasabel/orgs","repos_url":"https://api.github.com/users/andreasabel/repos","events_url":"https://api.github.com/users/andreasabel/events{/privacy}","received_events_url":"https://api.github.com/users/andreasabel/received_events","type":"User","site_admin":false},"created_at":"2016-09-18T12:55:17Z","updated_at":"2016-09-18T12:55:17Z","body":"Just a naive question from a spectator:  Why providing an equality for floats at all in Agda?  \r\nIt seems to encourage better programming practice to rather provide a library function that tests whether to floats are less than a threshold apart, i.e., that tests whether |x-y|<epsilon. "}}
{"actor":{"display_login":"andreasabel"}}