Variables

Variables used in equations can be declared beforehand. The scope of such variables is inside the module.

A variable is declared with the keyword var as follows:

var var-name : sort-name

Plural variables of the same sort can be declared with the keyword vars as follows:

vars var-name ... var-name : sort-name

NAT+ can be rewritten as follows:

mod! NAT+ {
  pr(SIMPLE-NAT)
  op _+_ : Nat Nat -> Nat
  vars N M : Nat
  eq 0 + M = M .
  eq s(N) + M = s(N + M) .
}