Most common errors during Mizaring

This should become a structured version of MizarPitfalls.

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

Setting the Environment

  • ConstructorsDirective?
  • NotationDirective?
  • ClustersDirective?
  • VocabularyDirective?

Type system

  • RedefinitionChasing?
  • ClusterChasing?


  • Trivialities not obvious to the checker


  • Mischievous Definitional Expansions
  • Unfriendly Schemes and Fraenkel Terms

-- WikiRoot - 05 Jul 2002

Topic revision: r2 - 2002-07-07 - 15:38:00 - WikiRoot
Mizar.StructuredPitfalls moved from Mizar.MizarPitfalls on 2002-07-07 - 15:36 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