[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] vocabularies
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