		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-cons-fields

Lift atj-gen-shallow-cons-field to lists.

Signature
(atj-gen-shallow-cons-fields conses qpairs) → fields
Arguments: conses — Guard (alistp conses).; qpairs — Guard (cons-pos-alistp qpairs).
Returns: fields — Type (jfield-listp fields).

A true list of consp pairs is actually an alistp, so we use that as the type of the first argument. However, it is treated as a list, not as an alist.

Definitions and Theorems

Function: atj-gen-shallow-cons-fields

(defun atj-gen-shallow-cons-fields (conses qpairs)
  (declare (xargs :guard (and (alistp conses)
                              (cons-pos-alistp qpairs))))
  (let ((__function__ 'atj-gen-shallow-cons-fields))
    (declare (ignorable __function__))
    (cond ((endp conses) nil)
          (t (cons (atj-gen-shallow-cons-field (car conses)
                                               qpairs)
                   (atj-gen-shallow-cons-fields (cdr conses)
                                                qpairs))))))

Theorem: jfield-listp-of-atj-gen-shallow-cons-fields

(defthm jfield-listp-of-atj-gen-shallow-cons-fields
  (b* ((fields (atj-gen-shallow-cons-fields conses qpairs)))
    (jfield-listp fields))
  :rule-classes :rewrite)