• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Std/util
    • Apt
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
      • Evmac-input-hints-p
      • Function-definedness
      • Event-macro-input-processing
      • Event-macro-screen-printing
      • Evmac-input-print-p
      • Make-event-terse
      • Event-macro-applicability-conditions
      • Event-macro-results
      • Template-generators
        • Template-fn-params
        • Template-fn-nonrecursive
        • Gen-template-fn-nonrecursive
      • Event-macro-event-generators
      • Event-macro-proof-preparation
      • Try-event
      • Restore-output?
      • Restore-output
      • Fail-event
      • Cw-event
      • Event-macro-xdoc-constructors
      • Event-macro-intro-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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)