[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] Environment Declaration




I have changed the subject because most of the messages with the subject "local DB" have nothing to do with local DB.

Josef Urban wrote:


Actually one thing that is a bit similar to the "theorems" solution would be to try to automatically construct the "vocabularies" directive from available "notations". The problem with that is that the parser now really needs to know the set of "symbols" beforehand (also for the notation newly defined in the article). Question is, whether that again could not be replaced by some initial shallow scan (possibly with some small syntax modification, making such scan easier). I wonder how much is it actually used in current MML to "cut off" some notation because its symbol is not mentioned in the "vocabularies" (and how easy would it be to fix such situations). Then only "notations","constructors","registrations" and "definitions" would remain.

I do not know the statistics, probably some modification of ACCOM may be used to get it. It happened few times that I have got the error #830 (nothing imported from notations not because constructors were missing in the environment but because the lack if an vocabulary. It was very confusing, I had kept adding the file names to the 'constructors' directive, but of course nothing changed. Eventually I make a discovery , oh probably a vocabulary needed. It is confusing because it is so rare.

Andrzej