{"action":"closed","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/856","labels_url":"https://api.github.com/repos/leanprover/lean/issues/856/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/856/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/856/events","html_url":"https://github.com/leanprover/lean/issues/856","id":113101797,"number":856,"title":"Tricky elaboration problems","user":{"login":"dselsam","id":4520285,"avatar_url":"https://avatars.githubusercontent.com/u/4520285?v=3","gravatar_id":"","url":"https://api.github.com/users/dselsam","html_url":"https://github.com/dselsam","followers_url":"https://api.github.com/users/dselsam/followers","following_url":"https://api.github.com/users/dselsam/following{/other_user}","gists_url":"https://api.github.com/users/dselsam/gists{/gist_id}","starred_url":"https://api.github.com/users/dselsam/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dselsam/subscriptions","organizations_url":"https://api.github.com/users/dselsam/orgs","repos_url":"https://api.github.com/users/dselsam/repos","events_url":"https://api.github.com/users/dselsam/events{/privacy}","received_events_url":"https://api.github.com/users/dselsam/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":8,"created_at":"2015-10-23T21:16:38Z","updated_at":"2015-12-11T15:38:55Z","closed_at":"2015-12-11T15:38:54Z","body":"Every once in a while the elaborator fails for a mysterious reason, though I am usually able to print everything and add implicit arguments to work around these failures. I think that given the extreme difficulty of the elaboration problem, these workarounds are completely reasonable, and it is rarely worth even trying to figure out why elaboration failed. \r\n\r\nTo reiterate, I am not suggesting we try to investigate more deeply nor modify the elaborator at all. However, there might come some point in the future where somebody might want to try to do so, and these problematic cases seem like they might eventually provide some value.\r\n\r\nIs there any sense in setting up a wiki as part of this repository where users can post elaboration problems that failed for mysterious reasons?"}}