Most common errors during Mizaring

(add your negative experience, create new topics; check the ErrorMessages, FeatureBrainstorming and MizarQuestions topics)

Some categorized listing should be eventually created in StructuredPitfalls.

New brainstorming topic (use a WikiWord title):

Results from Mizar web retrieved at 12:00 (GMT)

It seems that the current implementation does not allow a FunctorCluster for a RedefinedFunctor. This may be a serious problem, if a function is redefined immediately ...
The order of articles in the NotationDirective is important. If two definitions of the same symbol from two different articles mentioned in notation are applicable ...
Despite the permissive defintion of the type Element http://mizar.uwb.edu.pl/JFM/Vol1/subset 1.abs.html#M1 the Frankel term still requires its arguments to widen into ...
Number of topics: 3

Related topics: StructuredPitfalls, ErrorMessages

Topic revision: r1 - 2002-07-07 - 15:35:00 - WikiRoot
Mizar.MizarPitfall moved from Mizar.PitfallsList on 2002-07-07 - 15:38 by WikiRoot - put it back
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback