;;; $Id: nat-leq-mod.scm,v 1.2 2006/01/05 22:24:09 leavens Exp $
;;; AUTHOR: Tongjie Chen and Gary T. Leavens

(module nat-leq-mod (lib "typedscm.ss" "typedscm")

  (provide nat-leq)
  
  (require (lib "sub1-mod.scm" "lib342"))

  (deftype nat-leq (-> (number number) boolean))
  (define nat-leq
    (lambda (n1 n2)
      ;; REQUIRES: n1 and n2 are natural numbers
      ;; ENSURES: Result is #t just when n1 is less than or equal to n2
      (or (zero? n1)
          (and (not (zero? n2))
               (nat-leq (sub1 n1) (sub1 n2))))))
)