This commit is contained in:
Isaac Shoebottom 2025-01-29 11:41:03 -04:00
parent 89a6c652f9
commit 6c90e1435f

42
Labs/03.rkt Normal file
View File

@ -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