diff --git a/Labs/03.rkt b/Labs/03.rkt new file mode 100644 index 0000000..1ab20bb --- /dev/null +++ b/Labs/03.rkt @@ -0,0 +1,42 @@ +#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 \ No newline at end of file