		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.