[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Private DB
Hi Josef,
>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)?
Maybe "extends"?
Yes, I agree that whatever you call it, it should include the
stuff in the article itself too.
>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.
I don't know: redefinitions are often used to make the typing
of operations more specific, and those redefinitions have to
come after the original definition too. That's a matter of
ordering on the notations as well, I think? So it's not just
a matter of choosing non-ambiguous notation.
>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.
I don't know about this, I very much like the freedom that
Mizar gives you to re-use notation all the way you want, I
would hate it if that would be restricted in some way.
Freek