Introduction
How to use CafeOBJ processor: Start and Quit; Describing specifications; Reading specifications
Fundamentals of CafeOBJ: Comments; Modules; Sorts; Imports; Operators; Equations; Variables; Show; Parse; Reduce
Verification with proof scores: Proof scores; Equality predicate =; Associativity of +; Commutativity of +
Appendix: Troubleshooting; Built-in modules; Exercises

Show

The show command is used for showing a described module as follows:

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 system may give default attributes when some attributes are omitted. In the above case, the default strategy for the operator _+_ is given by the system.

[Next] Parse