next up previous contents
Next: The basic session model Up: Implementing algebraic logic in Previous: Implementing algebraic logic in

A brief introduction to declarations

Constant atomic terms and non-variable operators must be declared before being used in a theory. We will see below that it is permitted and sometimes important to declare variable operators. It is neither necessary nor possible to declare free or bound variables.

Equational axioms can be introduced by a simple command exhibited below in the first example. There are more complex commands discussed below for introducing constants and operators by definition.

Randall Holmes