Ideas and Brainstorming

The place for brainstorming around Mizar and Mizar technology in general. NOTE: Start a new topic for each idea.

New brainstorming topic (use a WikiWord title):

Results from Mizar web retrieved at 17:54 (GMT)

XML for Mizar and MML See http://ktiml.mff.cuni.cz/~urban/mizxml.ps for description of Mizar XML ization. See MizarXmlImplementation for implementation notes. JosefUrban ...
FunctorSynonyms The definition of dist(x,y) could be just a synonym. With appropriate clusters, the result type of (the distance of M).(x,y) is a real number already ...
An Attempt to Find Consensus about Indenting Rules for Mizar Block Rules proof, now, hereby, suppose, case should increase indentation, end; should decrease it, ...
Let's document the discussion about Mizar structures St. like "strict independence" (maybe property?) of some constructors would be quite useful; I am having the following ...
How to do Computer Algebra in Mizar Problem description Eventually, users will want to have things like inverse matrix for concrete 5x5 matrices quickly available ...
Removing non clusterable attributes, cluster mechanism propositions JosefUrban 07 Jul 2002
Mechanisms identifying, implying or interpreting theorems between intuitively "similar" notions should be discussed in general. As of the current Mizar, I would include ...
Renaming lables, indentation suggestions, etc. JosefUrban 07 Jul 2002
FraenkelTerms, LambdaTerms in Mizar?, features wanted, their implementation JosefUrban 07 Jul 2002
TestFeature WikiRoot 04 Jul 2002
Number of topics: 10

Related topics: WebHome, BrainstormScratchPad?, FeatureEnhancementRequests?, FeatureToDo?, FeatureUnderConstruction?, FeatureDone?, FeatureNotSuitable?

Topic revision: r1 - 2002-07-04 - 18:17:00 - WikiRoot
 
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