term-rewrite-system/tests/peano.scm

(use-modules (trs examples))
(use-modules (srfi srfi-64))

(define (number->peano n)
  (if (= n 0)
      '(z)
      `(s ,(number->peano (- n 1)))))

(test-begin "peano")
(test-equal (peano `(+ ,(number->peano 10)
                       ,(number->peano 4)))
  (number->peano 14))
(test-equal (peano `(* ,(number->peano 8)
                       ,(number->peano 7)))
  (number->peano 56))
(test-equal (peano `(* ,(number->peano 10)
                       ,(number->peano 7)))
  (number->peano 70))
(test-equal (peano `(* ,(number->peano 8)
                       ,(number->peano 10)))
  (number->peano 80))
(test-equal (peano `(* ,(number->peano 12)
                       ,(number->peano 10)))
  (number->peano 120))
(test-equal (peano `(* ,(number->peano 11)
                       ,(number->peano 13)))
  (number->peano 143))
(test-equal (peano `(* ,(number->peano 21)
                       ,(number->peano 23)))
  (number->peano 483))
(test-equal (peano `(* ,(number->peano 28)
                       ,(number->peano 27)))
  (number->peano 756))
(test-end "peano")