Equations

A term is constructed from operators and variables. An equation consists of a pair of terms (with or without a term of condition).

An equation is declared with the keyword eq as follows:

eq <lhs> = <rhs> .

Terms <lhs> and <rhs> should be of the same sort. Those terms can include variables.

Example (the first equation of NAT+)

eq 0 + M:Nat = M .

The symbol M stands for a variable of Sort Nat. The following equations can be deduced from the above equation:

Conditional equations

A conditional equation is declared with ceq as follows:

ceq <lhs> = <rhs> if <condition> .

A condition (<condition>) is a term of Sort Bool which is declared in the built-in module BOOL