MizarPitfall < Mizar < Mizar TWiki

Mizar

Mizar.MizarPitfallr1.1 - 07 Jul 2002 - 15:35 - WikiRoottopic end

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.

Results from Mizar web

RedefinedFunctorClusters

JosefUrban

18 Jul 2002 - 11:46 - r1.2

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 ...

NotationDirectiveOrder

JosefUrban

12 Jul 2002 - 12:56 - NEW

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 ...

FraenkelNonEmpty

WikiRoot

07 Jul 2002 - 15:52 - NEW

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 ...

Number of topics: 3

Related topics: StructuredPitfalls, ErrorMessages

to top

End of topic
Skip to action links | Back to top

Mizar.MizarPitfall moved from Mizar.PitfallsList on 07 Jul 2002 - 15:38 by WikiRoot - put it back

You are here: Mizar > MizarPitfall

to top