		Search-engine friendly clone of the ACL2 documentation.

Resize-list

List resizer in support of stobjs

(Resize-list lst n default-value) takes a list, lst, and a desired length, n, for the result list, as well as a default-value to use for the extra elements if n is greater than the length of lst.

Resize-list has a guard of t. This function is called in the body of function, resize-<a> where <a> is an array field of a stobj. See defstobj.

Function: resize-list-exec

(defun resize-list-exec (lst n default-value acc)
 (declare (xargs :guard (true-listp acc)))
 (if (and (integerp n) (> n 0))
     (resize-list-exec (if (atom lst) lst (cdr lst))
                       (1- n)
                       default-value
                       (cons (if (atom lst) default-value (car lst))
                             acc))
   (reverse acc)))

Function: resize-list

(defun resize-list (lst n default-value)
  (declare (xargs :guard t))
  (mbe :logic
       (if (and (integerp n) (> n 0))
           (cons (if (atom lst) default-value (car lst))
                 (resize-list (if (atom lst) lst (cdr lst))
                              (1- n)
                              default-value))
         nil)
       :exec (resize-list-exec lst n default-value nil)))

Subtopics

Std/lists/resize-list: Lemmas about resize-list available in the std/lists library.