# A Practical Guide To Mizar/The Environment

The environment of a Mizar article is in a sense the most difficult part to get right. That's why sometimes authors just copy the environment of existing articles and modify them to their needs.
The keywords under environ are called environment directives and their order is not specified by the Mizar Syntax. But there is a tradition of keeping to the following order:
* vocabularies
* notations
* constructors
* registrations
* requirements
* definitions
* equalities
* expansions
* theorems
* schemes
As seen in Installation none of these are mandatory for an article, but you are very likely to use the first five ones as well as theorems and sometimes schemes. definitions, equalities and expansions are basically syntactic sugar.
All articles listed behind an environment directive are written in ALL CAPS, separated by , and the directive ends with a ;.

## Vocabularies

Besides the Mizar keywords there are a lot of words that can have a certain meaning in your article, called symbols. They are kept in .voc files (which are plain text) associated with articles. For example, the tarski.voc looks like this:
Note that each symbol in the file is prefixed with a single letter that indicates the type of the symbol and the symbol after O can be followed by a number. We will get into that later. For now recognize that this means the vocabulary of TARSKI consists of the three words c=, union and are_equipotent (without the prefix letters or the suffix number). To use the words in your article (devoid of any meaning for now), write:
Since vocabularies only denotes the symbols to be imported without meaning attached to them, it is not uncommon to have articles in your vocabularies directive that don't show up in any other directive. For example, SEMI_AF1 has sum in its vocabulary, a very basic symbol. If you are not interested in Semi-Affine Spaces, you will never see it in any other directive.

### findvoc

Any symbol is defined in exactly one vocabulary file, so sometimes you need to search where the symbol you want to use comes from. Luckily, Mizar has a command for that: findvoc myvoc lists all articles that have a symbol containing the string myvoc, with that symbol written out. findvoc -w myvoc looks for a symbol myvoc and will return at most one article. For more options, execute the command findvoc. For example, findvoc -w sum has an output like this:
findvoc is case-sensitive.

### listvoc

To get all symbols defined in a vocabulary file, the listvoc myarticle command can be used. For example, listvoc HIDDEN has an output like this:
listvoc is case-insensitive, i.e. listvoc myarticle returns the same as listvoc MYARTICLE.

### HIDDEN

HIDDEN is, as the name implies, hidden and does not need to be included in your vocabulary directive ever, because it is automatically there.

## notations

The notations directive is what gives the symbols imported with vocabularies meaning. If the mathematical notation you want to use is defined in an article, that article is included in notations. If you want to use the c= notation from TARSKI for example, your code might look like this:
However, running mizf text/test now reports an error:
Your Mizar article now looks like this:
Mizar is complaining that apparently no notation from the cited article is used in yours. You can get rid of that error by adding the cited article to constructors as well. Some authors just put everything they put in notations also in constructors, but this behavior is discouraged, as it is often not needed.
The following article compiles again without errors:
HIDDEN is included automatically.

## Theorems

The theorems directive is filled with all articles from which you use theorems with the by keyword, like TARSKI:1 or TARSKI:def 1. So your article could look like this:
This article compiles. It will not if you leave theorems TARSKI; out of it.