| Mizar-Article = | ||
| environ | ||
| Environment-Declaration | ||
| begin | ||
| Text-Proper . | ||
Mizar Article can be considered as an extremely detailed mathematical text, written in the fixed formal language. Usually, its source is a text file which name is equipped with an obligatory extension .miz. The goal of writing a Mizar Article is to prove some claims and to introduce some new notions, based on the facts and concepts built in the Mizar System or gathered in a library.
Each Mizar Article consists of two parts. In the Environment Declaration the information of what should be imported from the library is specified. Text Proper contains theorems and definitions.
The division of a Mizar Article into two parts has one more technical meaning. Those two parts of a Mizar Article are processed by two different programs:
The shortest possible Mizar Article is:
environ begin |
A bit longer, but still correct:
environ
vocabularies ARYTM, XCMPLX_0;
constructors ARYTM_0, XCMPLX_0;
notations ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0;
requirements ARITHM, BOOLE;
registrations ORDINAL1, XCMPLX_0;
begin
for k being complex number holds k + 0 = k;
|
For more elaborate examples look into Journal of Formalized Mathematics.
Last modified: November 21, 2007