{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/792","labels_url":"https://api.github.com/repos/leanprover/lean/issues/792/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/792/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/792/events","html_url":"https://github.com/leanprover/lean/issues/792","id":100393514,"number":792,"title":"Namespaces and choice","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":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-08-11T19:47:19Z","updated_at":"2015-08-17T20:16:30Z","closed_at":null,"body":"The following works:\r\n\r\n```Lean\r\nopen nat\r\ndefinition zero := bool.ff\r\neval zero + succ zero\r\n```\r\nif and only if there are no active namespaces. The reason is that if a name is found in an active namespace, it is committed to without the possibility of choice:\r\n\r\nhttps://github.com/leanprover/lean/blob/master/src/frontends/lean/parser.cpp#L1271-L1281\r\n\r\nwhile on the other hand if an exact name is given, aliases are tried as backup options:\r\n\r\nhttps://github.com/leanprover/lean/blob/master/src/frontends/lean/parser.cpp#L1297-L1310\r\n\r\nWhat is the rationale for the different behavior?"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/131947496","html_url":"https://github.com/leanprover/lean/issues/792#issuecomment-131947496","issue_url":"https://api.github.com/repos/leanprover/lean/issues/792","id":131947496,"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-08-17T20:16:30Z","updated_at":"2015-08-17T20:16:30Z","body":"I have thought about this for a minute or two, but I am finding it hard to form an opinion. In all the time I have been using Lean, I don't think I have ever come across something I took to be unintuitive in this regard.\r\n\r\nThe proposal only seems to effect a very special case, e.g. I define \"empty\" at top level in the current file and there is also finset.empty in the context.\r\n\r\nI would suggest leaving it alone until someone has a strong opinion that it should be changed."}}