定義済みモジュールの宣言を表示するには show を使う:
CafeOBJ> show NAT+
module! NAT+
{
imports {
protecting (SIMPLE-NAT)
}
signature {
op _ + _ : Nat Nat -> Nat { strat: (1 0 2) }
}
axioms {
eq 0 + M:Nat = M .
eq s(N:Nat) + M:Nat = s(N + M) .
}
}
CafeOBJ> CafeOBJ は読み込んだ仕様のオペレータに対して、自動的にデフォルトの属性を付ける。show コマンドはそれらの属性を確認するときに便利である (通常は気にしなくてよい) 。上記の例では、オペレータ _+_ に E戦略による簡約順序が追加されている。
Original Copyright © Takahiro Seino, all rights reserved.