{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/1032","repository_url":"https://api.github.com/repos/leanprover/lean","labels_url":"https://api.github.com/repos/leanprover/lean/issues/1032/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/1032/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/1032/events","html_url":"https://github.com/leanprover/lean/issues/1032","id":143960595,"number":1032,"title":"Error in lean-checker","user":{"login":"spl","id":54900,"avatar_url":"https://avatars.githubusercontent.com/u/54900?v=3","gravatar_id":"","url":"https://api.github.com/users/spl","html_url":"https://github.com/spl","followers_url":"https://api.github.com/users/spl/followers","following_url":"https://api.github.com/users/spl/following{/other_user}","gists_url":"https://api.github.com/users/spl/gists{/gist_id}","starred_url":"https://api.github.com/users/spl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/spl/subscriptions","organizations_url":"https://api.github.com/users/spl/orgs","repos_url":"https://api.github.com/users/spl/repos","events_url":"https://api.github.com/users/spl/events{/privacy}","received_events_url":"https://api.github.com/users/spl/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2016-03-28T12:03:08Z","updated_at":"2016-03-28T13:42:00Z","closed_at":null,"body":"The following code causes the lean-checker error below.\r\n\r\n```lean\r\nimport data.finset\r\nopen setoid subtype\r\n\r\ntheorem finset.to_list {A : Type} (s : finset A) : list A :=\r\n  quot.hrec_on s elt_of (λ(a b : nodup_list A) (p : a ≈ b), by unfold elt_of)\r\n```\r\n\r\n```\r\nSuspicious state from syntax checker lean-checker:\r\nChecker lean-checker returned non-zero exit code 1, but no errors from output:\r\n[4/10] generating dep... /Users/spl/projects/flycheck_error.d               \r\n\r\nChecker definition probably flawed.\r\n```"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/202398191","html_url":"https://github.com/leanprover/lean/issues/1032#issuecomment-202398191","issue_url":"https://api.github.com/repos/leanprover/lean/issues/1032","id":202398191,"user":{"login":"fpvandoorn","id":7376012,"avatar_url":"https://avatars.githubusercontent.com/u/7376012?v=3","gravatar_id":"","url":"https://api.github.com/users/fpvandoorn","html_url":"https://github.com/fpvandoorn","followers_url":"https://api.github.com/users/fpvandoorn/followers","following_url":"https://api.github.com/users/fpvandoorn/following{/other_user}","gists_url":"https://api.github.com/users/fpvandoorn/gists{/gist_id}","starred_url":"https://api.github.com/users/fpvandoorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fpvandoorn/subscriptions","organizations_url":"https://api.github.com/users/fpvandoorn/orgs","repos_url":"https://api.github.com/users/fpvandoorn/repos","events_url":"https://api.github.com/users/fpvandoorn/events{/privacy}","received_events_url":"https://api.github.com/users/fpvandoorn/received_events","type":"User","site_admin":false},"created_at":"2016-03-28T13:42:00Z","updated_at":"2016-03-28T13:42:00Z","body":"I might be off here, but are you recompiling the standard library after just updating and building Lean?\r\n\r\nIn that case, this could be caused by still having old compiled files around. This should be solved by running `git clean -Xf && linja` in the `lean/library` folder (this requires `lean/bin` to be in `PATH`)."}}