- Equality is reflexive, symmetric, and transitive (for any type):

`refl``sym``trans` - Carry equality to more complicated terms

`absThm``appThm` - Replace a statement by an equivalent statement:

`eqMp`

A λ-abstraction
applied to an argument is equal to the result of substituting the argument:

`betaConv`

- Implication is transitive.

`proveHyp` - Implication is antisymmetric.
Mutual implication implies equivalence.

`deductAntisym` - Implication is reflexive. A statement implies itself.

`assume`

- Introduce an
*assumption*, which can be an unproved axiom or a statement to be proved in another article and to be imported from there:

`axiom`

- Mark a
*theorem*that has been derived for export, to be listed as a result of the theory or to be used in other articles:

`thm`

- A constant can be introduced by giving just a name, with the
intention of referring to a constant defined in another package or article.

`const` - A constant can be introduced as an
*abbreviation*for another more complicated expression. Its definition becomes a theorem, and it can be used in other packages or articles.

`defineConst`Several constants can be defined simultaneously, and this is combined with a substitution in a theorem:

`defineConstList` - In
the
`defineTypeOp`operation, two constants for the representation and abstraction function (rep and abs) are implicitly defined.

When a constant of the second and third category is defined,
a `Const` object is generated on the stack.
To use such a constant several times, this object
must be saved to the dictionary and retrieved from there.

When comparing two terms for α-equivalence,
constants of the first category are considered equal if they have the
same name (and type).
Constants of the second category are considered equal if they have the
same name and were introduced with the same definition (up to
α-equivalence?) including identical types.
Constants of the third category are considered equal if they originate
from the same `defineTypeOp` operation?
(and have the same type).
Constants of different categories are never considered equal.

It is possible to define and use different constants with the same name. However
it is illegal to use two or more such constants which are not equal by
the above rules in
the *assumptions* and *theorems* that are the result of
reading the article.

Types are built up from more elementary types by using
type operators. Type variables and nullary type operators are used as the basic building
blocks. The following command applies a type operator to its argument
types.

`opType`

Type variables

`varType`

Similar as for constants, there are two ways to make a type operator:

- By name

`typeOp` - By an explicit definition

`defineTypeOp`

This definition implicitly defines also two constants`rep`and`abs`, as mentioned above.

Deconstruction into head and tail:

`hdTl`

Strings
are used as names for variables, constants, type variables,
and type operators;
in addition, they can be arguments for
the `pragma` command.

Numbers
are used as indices into the dictionary; and
as an argument of the `version` command.
(In addition, they might be arguments for
the `pragma` command in future versions.)

Günter Rote, Aug 2015