#lang plait
(define-type Nat
  [Z]
  [S (pred : Nat)])
  
(define (plus nat1 nat2)
  (type-case Nat nat1
    [(Z) nat2]
    [(S pred) (S (plus pred nat2))]))

(define (compare nat1 nat2)
  (type-case Nat nat1
    [(Z)
     (type-case Nat nat2
       [(Z) 'equal]
       [(S pred) 'less])]
    [(S pred1)
     (type-case Nat nat2
       [(Z) 'greater]
       [(S pred2) (compare pred1 pred2)])]))

(define (times nat1 nat2)
  (type-case Nat nat1
    [(Z) (Z)]
    [(S pred)
     (type-case Nat nat2
       [(Z) (Z)]
       [(S pred2) (plus nat2 (times pred nat2))])]))

(test (plus (Z) (S (Z))) (S (Z)))
(test (plus (S (Z)) (Z)) (S (Z)))
(test (compare (Z) (Z)) 'equal)
(test (compare (Z) (S (Z))) 'less)
(test (compare (S (Z)) (Z)) 'greater)
(test (compare (S (S (Z))) (S (Z))) 'greater)
(test (times (Z) (Z)) (Z))
(test (times (Z) (S (Z))) (Z))
(test (times (S (Z)) (Z)) (Z))
(test (times (S (S (Z))) (S (Z))) (S (S (Z)))) ; 2 x 1
(test (times (S (Z)) (S (S (Z)))) (S (S (Z)))) ; 1 x 2
(test (times (S (Z)) (S (Z))) (S (Z))) ; 1 x 1
(test (times (S (S (Z))) (S (S (Z)))) (S (S (S (S (Z)))))) ; 2 x 2