{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/699","labels_url":"https://api.github.com/repos/leanprover/lean/issues/699/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/699/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/699/events","html_url":"https://github.com/leanprover/lean/issues/699","id":90759035,"number":699,"title":"define something in root namespace while in a namespace","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},"labels":[{"url":"https://api.github.com/repos/leanprover/lean/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-06-24T18:57:43Z","updated_at":"2015-06-28T20:30:38Z","closed_at":null,"body":"This is a very minor issue, but it would be nice if we could define something in the root namespace when we are currently in a namespace. This is especially useful when you're also currently in a section. Something like:\r\n\r\n```lean\r\nnamespace foo\r\n  section\r\n  definition _root_.bar := _\r\n  end\r\nend foo\r\n```\r\nCurrently a workaround is to define an abbreviation after the section and namespace are closed.\r\n"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/116328680","html_url":"https://github.com/leanprover/lean/issues/699#issuecomment-116328680","issue_url":"https://api.github.com/repos/leanprover/lean/issues/699","id":116328680,"user":{"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},"created_at":"2015-06-28T20:30:38Z","updated_at":"2015-06-28T20:30:38Z","body":"I have been thinking about this one.\r\nI think this is not a nice feature. It is adding more complexity to the namespace management system for a problem that can be solved existing features (e.g., `abbreviations` and `export` command).\r\nIn the current system, if we define `bar.boo` in the namespace `foo`, we are defining `foo.bar.boo`, but the metadata is stored in `foo` instead of `foo.bar`.\r\nWith this change, we have an exception when `bar` is `_root_`. First, the definition goes to a different place, we would also have to decide where the metadata goes. What about `_root_.bar.boo`? \r\n\r\nWe have the `export` command for moving data and metadata across namespaces. We should use it.\r\n\r\nBTW, we should improve the `export` command. It currently creates an abbreviation, but it should create an alias.\r\n"}}