		Search-engine friendly clone of the ACL2 documentation.

Untranslate-for-execution

Match-cons-nest

Matches (cons x1 (cons ... (cons xn 'nil))).

Signature
(match-cons-nest x) → (mv matchp args)
Arguments: x — Guard (ute-term-p x).
Returns: matchp — Type (booleanp matchp).; args — Type (ute-termlist-p args), given the guard.

Definitions and Theorems

Function: match-cons-nest

(defun match-cons-nest (x)
       (declare (xargs :guard (ute-term-p x)))
       (let ((__function__ 'match-cons-nest))
            (declare (ignorable __function__))
            (if (and (consp x) (eq (car x) 'cons))
                (mv-let (matchp acc)
                        (match-cons-nest-aux x nil)
                        (mv matchp (rev acc)))
                (mv nil nil))))

Theorem: booleanp-of-match-cons-nest.matchp

(defthm booleanp-of-match-cons-nest.matchp
        (b* (((mv ?matchp ?args)
              (match-cons-nest x)))
            (booleanp matchp))
        :rule-classes :type-prescription)

Theorem: ute-termlist-p-of-match-cons-nest.args

(defthm ute-termlist-p-of-match-cons-nest.args
        (implies (and (ute-term-p x))
                 (b* (((mv ?matchp ?args)
                       (match-cons-nest x)))
                     (ute-termlist-p args)))
        :rule-classes :rewrite)

Subtopics

Match-cons-nest-aux