Hons-make-list
Like make-list, but produces honses.
Definitions and Theorems
Function: hons-make-list-acc
(defun hons-make-list-acc (n val ac)
(declare (xargs :guard t))
(mbe :logic (make-list-ac n val ac)
:exec (if (not (posp n))
ac
(hons-make-list-acc (1- n)
val (hons val ac)))))
