#|

 Lab 2 Problem Set.

 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.

 Include the following directive at the top of your Lisp file:

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 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 maj. What should ?? be?

(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)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 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 the 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))