suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Added mult, exp; square via staging

Browse Source
This commit is contained in:
William J. Bowman 2016-01-08 22:54:31 -05:00
parent ca2b62fc70
commit 691b01e15a
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 23 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
stdlib/nat.rkt
View File

@ -30,6 +30,29 @@
(check-equal? (plus z z) z)
(check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
(define (mult (m : Nat) (n : Nat))
(match m
[z z]
[(s (x : Nat))
(plus n (recur x))]))
(module+ test
(check-equal? (mult (s (s z)) z) z)
(check-equal? (mult (s (s z)) (s z)) (s (s z))))
(define (exp (m : Nat) (e : Nat))
(match m
[z (s z)]
[(s (x : Nat))
(mult e (recur x))]))
(module+ test
(check-equal? (exp z z) (s z))
(check-equal? (exp (s (s z)) z) z))
(define square (run (exp (s (s z)))))
;; TODO: This test takes too long t run
#;(module+ test
(check-equal? (square (s (s z))) (s (s (s (s z))))))
;; Credit to this function goes to Max
(define nat-equal?
(elim Nat Type (lambda (x : Nat) (-> Nat Bool))