;; illustrating definec:


;; rl: TL x Nat -> TL
;; Given a list, l, and a natural number, n,
;; rl rotates the list to the left n times


;; first attempt:
(definec rl (l :tl n :nat) :tl
  (if (endp l)
     nil
     (rl (app (rest l) (list (first l))) (- n 1))))


;; second attempt:
(definec rl (l :tl n :nat) :tl
  (if (equal n 0)
     l
     (rl (app (rest l) (list (first l))) (- n 1))))

;; these tests pass:
(check= (rl (list 1 2 3) 1) (list 2 3 1))
(check= (rl (list 1 2 3) 2) (list 3 1 2))
(check= (rl (list 1 2 3) 3) (list 1 2 3))

;; but this test fails:
(check= (rl () 3) ())


;; third attempt:
(definec rl (l :tl n :nat) :tl
  (cond
     ((equal n 0) l)
     ((endp l) nil)
     (t (rl (app (rest l) (list (first l))) (- n 1)))))

;; all these tests pass:
(check= (rl () 3) ())
(check= (rl (list 1 2 3) 0) (list 1 2 3))
(check= (rl (list 1 2 3) 1) (list 2 3 1))
(check= (rl (list 1 2 3) 2) (list 3 1 2))
(check= (rl (list 1 2 3) 3) (list 1 2 3))