Re: vocabularies
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
On Mon, 5 Jan 2009, Freek Wiedijk wrote: > Hi Josef, > >>> To me this seems a much more drastic change than what I >>> was proposing. I guess it also would mean unifying the >>> vocabulary and article name spaces? >> >> I think there would be no "vocabulary". > > So all vocabularies would be always active? no, symbols (which need to be known beforehand by the existing Mizar parser) would be taken from - notations (which sort of contain them already now) - definitions inside the article (which might need some syntax change to allow easy parse of the new symbols) > Or would you want to introduce the vocabulary elements > together with the notation, always? yes > So that sounds a more > radical change than what I proposed. (My proposal was > just to move text from one file to another, but without > the system really changing.) yes; I think something really should be done with the environment "black magic"; perhaps even the "constructors" directive could be made only optional or removed totally; if this causes more notation clashes, then they should be resolved by renaming the overloaded symbols, not by resorting to black magic operations with the environment header Josef