{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/603","labels_url":"https://api.github.com/repos/leanprover/lean/issues/603/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/603/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/603/events","html_url":"https://github.com/leanprover/lean/issues/603","id":76910435,"number":603,"title":"esimp doesn't unfold everything","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":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2015-05-16T01:14:23Z","updated_at":"2015-05-16T02:55:39Z","closed_at":null,"body":"In [this file](https://github.com/fpvandoorn/lean/blob/issue603/hott/algebra/category/constructions/comma.hlean#L44-45) I write `esimp [ap011,ap] at r`, but not every occurrence of `ap` in `r` gets replaced (and actually `esimp` should already unfold both occurrences of `ap`, since it has the `unfold-c` attribute and it is applied to `refl`).\r\n\r\nI tried to make a minimal example, but in more minimal examples `ap` does get unfolded."},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/102566565","html_url":"https://github.com/leanprover/lean/issues/603#issuecomment-102566565","issue_url":"https://api.github.com/repos/leanprover/lean/issues/603","id":102566565,"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},"created_at":"2015-05-16T02:55:39Z","updated_at":"2015-05-16T02:55:39Z","body":"I'm already exporting pretty selectively: https://github.com/leanprover/lean/blob/master/hott/init/default.hlean#L17-26. And I think that making exported definitions `protected` defeats the purpose a bit. If you then write `core.ap`, you could just as well have written `eq.ap`.\r\n\r\nI think the main issue is that I had a misconception about the `export` command. I thought that if I write\r\n```lean\r\nnamespace core\r\n  export bool empty unit sum\r\nend core\r\n\r\nopen core\r\n```\r\nthis would be similar to\r\n```lean\r\nopen bool empty unit sum\r\n```\r\nbut it's not. Instead, all declarations are copied to the `core` namespace. \r\n\r\nI think it would be nice (but this is low priority and I don't know how feasible it is) if export doesn't actually copy declarations, but instead when I write `open core`, I open all the namspaces as specified by `export`. So I cannot write `core.tt` instead of `bool.tt`, but if I open `core`, there is an alias `tt` created for `bool.tt`.\r\n\r\nAre there reasons why the current behavior is more useful than what I'm suggesting?\r\n\r\nI'm closing this issue now. The original issue is resolved, and the rest is low priority, in my opinion."}}