#|

 To test your fresh installation of ACL2s, run this file.

 Make sure you are in ACL2s mode. This is essential! Note that you can
 only change the mode when the session is not running, so set the
 correct mode before starting the session.

 Hit the downwards arrow in ACL2s/eclipse ("Advance todo line") step by
 step until you reach the end of the file, to make sure all forms pass
 ACL2s.
 
|#

; a simple function definition:

(definec mylen (l :tl) :nat
  (if (endp l)
    0
    (+ 1 (mylen (cdr l)))))

(check= (mylen nil) 0)
(check= (mylen ()) 0)
(check= (mylen '()) 0)
(check= (mylen (list 1 2 3)) 3)
(check= (mylen '(1 2 3 4)) 4)#|ACL2s-ToDo-Line|#