{"action":"closed","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/586","labels_url":"https://api.github.com/repos/leanprover/lean/issues/586/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/586/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/586/events","html_url":"https://github.com/leanprover/lean/issues/586","id":74045139,"number":586,"title":"request: combine have/assert with calc","user":{"login":"htzh","id":5956967,"avatar_url":"https://avatars.githubusercontent.com/u/5956967?v=3","gravatar_id":"","url":"https://api.github.com/users/htzh","html_url":"https://github.com/htzh","followers_url":"https://api.github.com/users/htzh/followers","following_url":"https://api.github.com/users/htzh/following{/other_user}","gists_url":"https://api.github.com/users/htzh/gists{/gist_id}","starred_url":"https://api.github.com/users/htzh/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/htzh/subscriptions","organizations_url":"https://api.github.com/users/htzh/orgs","repos_url":"https://api.github.com/users/htzh/repos","events_url":"https://api.github.com/users/htzh/events{/privacy}","received_events_url":"https://api.github.com/users/htzh/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-05-07T16:25:52Z","updated_at":"2015-05-07T17:10:25Z","closed_at":"2015-05-07T17:10:25Z","body":"Right now we need to say:\r\n```\r\nhave P : A = C, from\r\ncalc A = B : eq1\r\n... = C : eq2\r\n```\r\nIt would be nice if we can simply say:\r\n```\r\nhave P calc A = B : eq1\r\n... = C : eq2\r\n```\r\nand the prover should register P: A = C as an intermediate result. This should promote short forward chain reasoning which I think is clearer than if I simply write out the same in function application style using subst. Also it would be nice to be able to forward chain implications, just like chaining equations in calc, maybe with a different command name such as \"imp\".\r\n"}}