定義済みモジュールの表示

定義済みモジュールの宣言を表示するには 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.