{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/1368","repository_url":"https://api.github.com/repos/leanprover/lean","labels_url":"https://api.github.com/repos/leanprover/lean/issues/1368/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/1368/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/1368/events","html_url":"https://github.com/leanprover/lean/pull/1368","id":206845603,"number":1368,"title":"Change induction, cases, and apply to return information how they changed the goal","user":{"login":"johoelzl","id":5176109,"avatar_url":"https://avatars.githubusercontent.com/u/5176109?v=3","gravatar_id":"","url":"https://api.github.com/users/johoelzl","html_url":"https://github.com/johoelzl","followers_url":"https://api.github.com/users/johoelzl/followers","following_url":"https://api.github.com/users/johoelzl/following{/other_user}","gists_url":"https://api.github.com/users/johoelzl/gists{/gist_id}","starred_url":"https://api.github.com/users/johoelzl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/johoelzl/subscriptions","organizations_url":"https://api.github.com/users/johoelzl/orgs","repos_url":"https://api.github.com/users/johoelzl/repos","events_url":"https://api.github.com/users/johoelzl/events{/privacy}","received_events_url":"https://api.github.com/users/johoelzl/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":1,"created_at":"2017-02-10T16:44:54Z","updated_at":"2017-02-10T21:13:35Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/leanprover/lean/pulls/1368","html_url":"https://github.com/leanprover/lean/pull/1368","diff_url":"https://github.com/leanprover/lean/pull/1368.diff","patch_url":"https://github.com/leanprover/lean/pull/1368.patch"},"body":"`induction` and `cases` return now information about added hypotheses and how they modified existing hypotheses. `apply` returns *all* generated mvars.\r\n\r\nWith this we do not need to analyze the applied rules beforehand, also we do not need to generate names used by `induction` and `cases`. It is also easy to check that the result is as expected (i.e. `do [[a, b]] <- cases r`).\r\n\r\nFor `apply` it may be important to know which mvars where generated and which ones are available in the generated subgoals. For some cases it can be hard to predict which mvars are assigned. This change should allow an easier map of rule parameters to subgoals."},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/279067241","html_url":"https://github.com/leanprover/lean/pull/1368#issuecomment-279067241","issue_url":"https://api.github.com/repos/leanprover/lean/issues/1368","id":279067241,"user":{"login":"johoelzl","id":5176109,"avatar_url":"https://avatars.githubusercontent.com/u/5176109?v=3","gravatar_id":"","url":"https://api.github.com/users/johoelzl","html_url":"https://github.com/johoelzl","followers_url":"https://api.github.com/users/johoelzl/followers","following_url":"https://api.github.com/users/johoelzl/following{/other_user}","gists_url":"https://api.github.com/users/johoelzl/gists{/gist_id}","starred_url":"https://api.github.com/users/johoelzl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/johoelzl/subscriptions","organizations_url":"https://api.github.com/users/johoelzl/orgs","repos_url":"https://api.github.com/users/johoelzl/repos","events_url":"https://api.github.com/users/johoelzl/events{/privacy}","received_events_url":"https://api.github.com/users/johoelzl/received_events","type":"User","site_admin":false},"created_at":"2017-02-10T21:13:35Z","updated_at":"2017-02-10T21:13:35Z","body":"I repushed. I undid all `>>=`, `>>` to `do` changes. I updated to documentation. Also, please check the C++ code: I did run `valgrind` on simple tests but this is my first time to write C++ in a long time."}}
{"actor":{"display_login":"johoelzl"}}