- ...TRIV
- TRIV is a built-in module in which only one sort
Elt is declared.
- ...NzNat
- The sort NzNat is declared in the
module NAT-VALUE imported into NAT and stands for non-zero
natural numbers.
- ...result
- 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.
Kazuhiro Ogata
Mon Nov 29 13:47:22 JST 1999