{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/621","labels_url":"https://api.github.com/repos/leanprover/lean/issues/621/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/621/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/621/events","html_url":"https://github.com/leanprover/lean/issues/621","id":79472759,"number":621,"title":"Abbreviations in tactic mode","user":{"login":"rlewis1988","id":4967469,"avatar_url":"https://avatars.githubusercontent.com/u/4967469?v=3","gravatar_id":"","url":"https://api.github.com/users/rlewis1988","html_url":"https://github.com/rlewis1988","followers_url":"https://api.github.com/users/rlewis1988/followers","following_url":"https://api.github.com/users/rlewis1988/following{/other_user}","gists_url":"https://api.github.com/users/rlewis1988/gists{/gist_id}","starred_url":"https://api.github.com/users/rlewis1988/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/rlewis1988/subscriptions","organizations_url":"https://api.github.com/users/rlewis1988/orgs","repos_url":"https://api.github.com/users/rlewis1988/repos","events_url":"https://api.github.com/users/rlewis1988/events{/privacy}","received_events_url":"https://api.github.com/users/rlewis1988/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/leanprover/lean/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":{"login":"leodemoura","id":2778936,"avatar_url":"https://avatars.githubusercontent.com/u/2778936?v=3","gravatar_id":"","url":"https://api.github.com/users/leodemoura","html_url":"https://github.com/leodemoura","followers_url":"https://api.github.com/users/leodemoura/followers","following_url":"https://api.github.com/users/leodemoura/following{/other_user}","gists_url":"https://api.github.com/users/leodemoura/gists{/gist_id}","starred_url":"https://api.github.com/users/leodemoura/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leodemoura/subscriptions","organizations_url":"https://api.github.com/users/leodemoura/orgs","repos_url":"https://api.github.com/users/leodemoura/repos","events_url":"https://api.github.com/users/leodemoura/events{/privacy}","received_events_url":"https://api.github.com/users/leodemoura/received_events","type":"User","site_admin":false},"milestone":null,"comments":6,"created_at":"2015-05-22T14:19:22Z","updated_at":"2015-05-23T22:16:52Z","closed_at":null,"body":"I'm close to finishing the construction of the reals- currently I've shown through commutative ring, with a few holes. The missing theorems have some annoying notation that would be nice to abbreviate. \r\n\r\nCurrently you can use 'let' to define new terms in tactic proofs, but this is only useful for props, as the data seems to be lost:\r\n```lean\r\nexample (a b : ℕ) : a = a :=\r\n  begin\r\n    let z := a,\r\n    --have H : z = a, from rfl,  -- this line doesn't work\r\n    apply refl\r\n  end\r\n```\r\n\r\nIs there a way to introduce an abbreviation using let (or something similar), and rewrite the context/goal using the new abbreviation?"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/104950993","html_url":"https://github.com/leanprover/lean/issues/621#issuecomment-104950993","issue_url":"https://api.github.com/repos/leanprover/lean/issues/621","id":104950993,"user":{"login":"avigad","id":2783534,"avatar_url":"https://avatars.githubusercontent.com/u/2783534?v=3","gravatar_id":"","url":"https://api.github.com/users/avigad","html_url":"https://github.com/avigad","followers_url":"https://api.github.com/users/avigad/followers","following_url":"https://api.github.com/users/avigad/following{/other_user}","gists_url":"https://api.github.com/users/avigad/gists{/gist_id}","starred_url":"https://api.github.com/users/avigad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/avigad/subscriptions","organizations_url":"https://api.github.com/users/avigad/orgs","repos_url":"https://api.github.com/users/avigad/repos","events_url":"https://api.github.com/users/avigad/events{/privacy}","received_events_url":"https://api.github.com/users/avigad/received_events","type":"User","site_admin":false},"created_at":"2015-05-23T22:16:52Z","updated_at":"2015-05-23T22:16:52Z","body":"\r\nHmmm. Floris, Jakob, Rob, and you have naturally gravitated towards long tactic proofs, and the proofs we do will get longer, so I guess in the long run it will make a difference."}}