Zero as String       ==> Zero
Err as String        ==> Err
three as String      ==> Succ(Succ(Succ(Zero)))
six as String        ==> Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))
big as String        ==> 100
bad as String        ==> -1
Nat.toNat(0)         ==> Zero
Nat.toNat(5)         ==> Succ(Succ(Succ(Succ(Succ(Zero)))))
Nat.toNat(big)       ==> Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Nat.toNat(bad)       ==> Err
Zero + Zero          ==> Zero
Zero + three         ==> Succ(Succ(Succ(Zero)))
Zero + Err           ==> Err
Zero - Zero          ==> Zero
Zero - three         ==> Err
Zero - Err           ==> Err
Zero == Zero         ==> true
Zero == three        ==> false
Zero == Err          ==> false
Zero == bad          ==> false
Zero < Zero          ==> false
Zero < three         ==> true
Zero < Err           ==> Error:  No ordering between Zero and Err
Zero <= Zero         ==> true
Zero <= Err          ==> Error:  No ordering between Zero and Err
Zero > Zero          ==> false
Zero > three         ==> false
Zero > Err           ==> Error:  No ordering between Zero and Err
Zero.pred            ==> Err
Zero.toInt           ==> 0
three + Zero         ==> Succ(Succ(Succ(Zero)))
three + three        ==> Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))
three + Err          ==> Err
three - Zero         ==> Succ(Succ(Succ(Zero)))
three - three        ==> Zero
three - six          ==> Err
three - Err          ==> Err
three == Zero        ==> false
three == three       ==> true
three == six         ==> false
three == Err         ==> false
three == bad         ==> false
three < Zero         ==> false
three < three        ==> false
three < six          ==> true
six   < three        ==> false
three < Err          ==> Error:  No ordering between Succ and Err
three <= Zero        ==> false
three <= three       ==> true
three <= six         ==> true
six   <= three       ==> false
three <= Err         ==> Error:  No ordering between Succ and Err
three > Zero         ==> true
three > three        ==> false
three > six          ==> false
six   > three        ==> true
three > Err          ==> Error:  No ordering between Succ and Err
three.pred           ==> Succ(Succ(Zero))
three.toInt          ==> 3
Err + Zero           ==> Err
Err + three          ==> Err
Err + Err            ==> Err
Err - Zero           ==> Err
Err - three          ==> Err
Err - Err            ==> Err
Err == Zero          ==> false
Err == three         ==> true
Err == Err           ==> true
Err == bad           ==> false
Err < three          ==> Error:  No ordering between Err and Succ(Succ(Succ(Zero)))
Err.pred             ==> Err
Err.toInt            ==> -1
new Succ(Err)        ==> Error on Succ constructor precondition check:  requirement failed