#|

 Lab 2 

 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.

 For each function definition, you must provide both contracts and a
 body.  You must also ALWAYS supply your own tests, and sufficiently
 many, in addition to the tests sometimes provided. The number of
 tests should reflect the data definitions relevant for the problem,
 and the difficulty of the function.

 Write tests using ACL2s' check= function.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; maj : Bool x Bool x Bool -> ??
;
; (maj a b c) is t if the "majority" (i.e. at least two) of a, b, c is t,
; and nil otherwise.
;
; Define the function maj: 

(definec maj ...
  )

(check= (maj nil t nil) nil)
(check= (maj t nil t) t)
...

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; n-times: TL x All x Nat  -> Bool
;
; (n-times l a n) returns t if l contains a exactly n times and nil otherwise.
;
; Define n-times

(definec n-times ...
  )
   
(check= (n-times '() 5 0) t)
(check= (n-times '(4 5) 5 1) t)
(check= (n-times '(4 5 4 5) 4 3) nil)


;; We may not have covered data definitions (defdata) by the time of
;; this lab. Read the lecture notes to see how defdata can be used
;; for the problems below.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Use defdata to define a list of natural numbers (Natlist)

(defdata natlist ...)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Use defdata to define a non-empty list of rationals (ne-lor)

(defdata ne-lor ...)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Use defdata to define a list of natural numbers or booleans
; (NatBoollist)

(defdata natboollist ...)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; count-bools: NatBoollist -> ??
;
; count-bools counts the number of booleans in a NatBoollist
;
; Define count-bools

(definec count-bools ...
  )

(check= (count-bools '(1 nil 4 5)) 1)
(check= (count-bools '(1 nil 4 2 5)) 1)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; compress : TL -> TL

; (compress l) replaces consecutive occurrences of an element
; by a single occurrence.
;
; Define compress

(definec compress 
  ...)

(check= (compress '(1 1 1 2 3 3 2 2 2 2)) '(1 2 3 2))