- TRIV is a built-in module in which only one sort
Elt is declared.
- The sort NzNat is declared in the
module NAT-VALUE imported into NAT and stands for non-zero
- The result is a reduct of the
term, but it might not be in normal form. For example, the result of
evaluating inf(1) is cons(1, inf(1+1)) that is not in
normal form w.r.t. TEST1.
Mon Nov 29 13:47:22 JST 1999