- ...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*.

Mon Nov 29 13:47:22 JST 1999