		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-*-comma-function-parameter

Abstract a *( "," function-parameter ) to a list of function parameters.

Signature
(abs-*-comma-function-parameter trees) → fpars
Arguments: trees — Guard (abnf::tree-listp trees).
Returns: fpars — Type (funparam-list-resultp fpars).

Definitions and Theorems

Function: abs-*-comma-function-parameter

(defun abs-*-comma-function-parameter (trees)
  (declare (xargs :guard (abnf::tree-listp trees)))
  (let ((__function__ 'abs-*-comma-function-parameter))
    (declare (ignorable __function__))
    (b* (((when (endp trees)) nil)
         ((okf fpar)
          (abs-comma-function-parameter (car trees)))
         ((okf fpars)
          (abs-*-comma-function-parameter (cdr trees))))
      (cons fpar fpars))))

Theorem: funparam-list-resultp-of-abs-*-comma-function-parameter

(defthm funparam-list-resultp-of-abs-*-comma-function-parameter
  (b* ((fpars (abs-*-comma-function-parameter trees)))
    (funparam-list-resultp fpars))
  :rule-classes :rewrite)

Theorem: abs-*-comma-function-parameter-of-tree-list-fix-trees

(defthm abs-*-comma-function-parameter-of-tree-list-fix-trees
 (equal (abs-*-comma-function-parameter (abnf::tree-list-fix trees))
        (abs-*-comma-function-parameter trees)))

Theorem: abs-*-comma-function-parameter-tree-list-equiv-congruence-on-trees

(defthm
 abs-*-comma-function-parameter-tree-list-equiv-congruence-on-trees
 (implies (abnf::tree-list-equiv trees trees-equiv)
          (equal (abs-*-comma-function-parameter trees)
                 (abs-*-comma-function-parameter trees-equiv)))
 :rule-classes :congruence)