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) .
}