変数

前述したように、変数は等式中で宣言することができる。しかし、頻繁に使う変数はあらかじめまとめて宣言しておくと便利である。このように宣言した変数のスコープは、宣言したモジュール内である。

等式の外で変数を宣言するには varを使う:

var <var-name> : <sort-name>

同じソート上の複数の変数は varsを使って宣言できる:

vars <var-name> ... <var-name> : <sort-name>

vars を使うと NAT+ は次のように記述できる:

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