Hi Freek, On Mon, 18 Sep 2006, Freek Wiedijk wrote:
Hi Josef,I think that one simplified directive like "import all the topology stuff" would at least simplify starting a Mizar article on advanced topics. The practice today is first to think "what article is closest to my topic", and then to copy its environment. If someone new does the mistake of trying to understand the black magic behind environmental directives, he is probably lost as a Mizar author forever. The old directives could remain for fine-tuning if needed.Ah! Why not have a directive "copy", that gives you everything that is in the environment of an existing article? Then later you could extend that by adding "traditional" directives after it.
Yes, that seems quite easy to do. The only ambiguity is whether "copy FOO" should only import the environment declarations of FOO, or also the theorems, clusters, etc. introduced in FOO (btw., the "vocabularies" directive is already now pretty inconsistent with the rest of directives in this sense). So perhaps "needs", "import", or "include" could be less ambiguous (hopefully being understood as including FOO as well)?
Or wouldn't that work well, as you only would be able to extend the notations at the end?
I sincerely hate this sensitivity of "notations" (and "definitions") to the ordering of directives. In my opinion, something is wrong with the article, if such tweaking is needed. One thing is to allow overloaded notation for various parts of mathematics, but other thing is to manage the readability of that overloading. In my opinion Mizar has gone too far in allowing unreadable overloading. It should force authors to introduce and use nonambiguous synonyms when clash of notation occurs.
So the answer to your wuestion is that if it does not work well, it is because Mizar allows too much hackery, and it should be fixed.
Josef