{"action":"closed","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/561","labels_url":"https://api.github.com/repos/leanprover/lean/issues/561/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/561/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/561/events","html_url":"https://github.com/leanprover/lean/issues/561","id":70865465,"number":561,"title":"Bug in tutorial software (checked against Emacs/native Lean)","user":{"login":"fspeech","id":2243317,"avatar_url":"https://avatars.githubusercontent.com/u/2243317?v=3","gravatar_id":"","url":"https://api.github.com/users/fspeech","html_url":"https://github.com/fspeech","followers_url":"https://api.github.com/users/fspeech/followers","following_url":"https://api.github.com/users/fspeech/following{/other_user}","gists_url":"https://api.github.com/users/fspeech/gists{/gist_id}","starred_url":"https://api.github.com/users/fspeech/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fspeech/subscriptions","organizations_url":"https://api.github.com/users/fspeech/orgs","repos_url":"https://api.github.com/users/fspeech/repos","events_url":"https://api.github.com/users/fspeech/events{/privacy}","received_events_url":"https://api.github.com/users/fspeech/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":5,"created_at":"2015-04-25T06:35:56Z","updated_at":"2015-04-27T17:01:52Z","closed_at":"2015-04-27T17:01:52Z","body":"If I run\r\n```\r\ncheck (∀x, p x → r) ↔ (∃x, p x) → r\r\n```\r\nI get this type:\r\n```\r\n(∀x, p x → r) ↔ ∃ (x : A), p x → r\r\n```\r\ninstead. Sorry I couldn't capture the exact output. (Is there an option to print to console instead of getting a floating info frame? I don't know how to copy from the result frame).\r\nThis looks wrong to me. So I thought I proved the following \r\n```\r\n  example : (∀x, p x → r) ↔ (∃x, p x) → r :=\r\n    iff.intro\r\n        (assume (H : (∀x, p x → r)) (Hep : (∃x, p x)),\r\n            obtain x Hpx, from Hep, H x Hpx)\r\n        (assume (H : (∃x, p x) → r),\r\n            take x, assume px : p x,\r\n                H (exists.intro x px))\r\n```\r\nbut the web version won't accept it, as the type checking would indicate.\r\nI checked that the native Lean running through Emacs does not have this bug:\r\n```\r\n(∀ (x : A), p x → r) ↔ (∃ (x : A), p x) → r : Prop\r\n```\r\n"}}