		Search-engine friendly clone of the ACL2 documentation.

Template-generators

Template-fn-params

Parameters of a template function.

Signature
(template-fn-params n) → params
Arguments: n — Guard (natp n).
Returns: params — Type (symbol-listp params).

Return the list of symbols (x1 ... xn), where n is the argument of this utility. These symbols are used as formal parameters of template functions.

Definitions and Theorems

Function: template-fn-params-aux

(defun template-fn-params-aux (i n)
  (declare (xargs :guard (and (natp i) (natp n))))
  (let ((__function__ 'template-fn-params-aux))
    (declare (ignorable __function__))
    (let ((i (mbe :logic (nfix i) :exec i))
          (n (mbe :logic (nfix n) :exec n)))
      (if (> i n)
          nil
        (cons (add-suffix 'x
                          (str::nat-to-dec-string i))
              (template-fn-params-aux (1+ i) n))))))

Theorem: symbol-listp-of-template-fn-params-aux

(defthm symbol-listp-of-template-fn-params-aux
  (b* ((params (template-fn-params-aux i n)))
    (symbol-listp params))
  :rule-classes :rewrite)

Function: template-fn-params

(defun template-fn-params (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'template-fn-params))
    (declare (ignorable __function__))
    (template-fn-params-aux 1 n)))

Theorem: symbol-listp-of-template-fn-params

(defthm symbol-listp-of-template-fn-params
  (b* ((params (template-fn-params n)))
    (symbol-listp params))
  :rule-classes :rewrite)