(in-package "ACL2")

(defun build-property (gens prop)
  (if (endp gens) prop
    `(implies ,(caddr (car gens))
              ,(build-property (cdr gens) prop))))

(defmacro defproperty (name count gens prop &rest rest)
  (declare (ignore count))
  `(defthm ,name ,(build-property gens prop) ,@rest))

(defmacro defgenerator (name args &rest r)
  (declare (ignore r))
  `(defun ,name (,@args)
     (declare (xargs :guard nil))
     (list ,@args)))

(defgenerator random-int-between ())
(defgenerator random-size ())
(defgenerator random-boolean ())
(defgenerator random-char ())
(defgenerator random-list-of ())
(defgenerator random-string ())
(defgenerator random-list ())
(defgenerator random-symbol ())

(defun check-properties () t)