		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax

Statements-to-fundefs

Filter function definitions out of a list of statements.

Signature
(statements-to-fundefs stmts) → fundefs
Arguments: stmts — Guard (statement-listp stmts).
Returns: fundefs — Type (fundef-listp fundefs).

The function definitions are in the same order as they appear in the list of statements. We discard all the statements that are not function definitions, and we eliminate the :statement-fundef wrappers.

Definitions and Theorems

Function: statements-to-fundefs

(defun statements-to-fundefs (stmts)
  (declare (xargs :guard (statement-listp stmts)))
  (let ((__function__ 'statements-to-fundefs))
    (declare (ignorable __function__))
    (cond ((endp stmts) nil)
          ((statement-case (car stmts) :fundef)
           (cons (statement-fundef->get (car stmts))
                 (statements-to-fundefs (cdr stmts))))
          (t (statements-to-fundefs (cdr stmts))))))

Theorem: fundef-listp-of-statements-to-fundefs

(defthm fundef-listp-of-statements-to-fundefs
  (b* ((fundefs (statements-to-fundefs stmts)))
    (fundef-listp fundefs))
  :rule-classes :rewrite)

Theorem: statements-to-fundefs-of-statement-list-fix-stmts

(defthm statements-to-fundefs-of-statement-list-fix-stmts
  (equal (statements-to-fundefs (statement-list-fix stmts))
         (statements-to-fundefs stmts)))

Theorem: statements-to-fundefs-statement-list-equiv-congruence-on-stmts

(defthm
     statements-to-fundefs-statement-list-equiv-congruence-on-stmts
  (implies (statement-list-equiv stmts stmts-equiv)
           (equal (statements-to-fundefs stmts)
                  (statements-to-fundefs stmts-equiv)))
  :rule-classes :congruence)