		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