		Search-engine friendly clone of the ACL2 documentation.

Atj-shallow-quoted-constant-generation

Atj-gen-shallow-char-fields

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

Signature
(atj-gen-shallow-char-fields chars) → fields
Arguments: chars — Guard (character-listp chars).
Returns: fields — Type (jfield-listp fields).

Definitions and Theorems

Function: atj-gen-shallow-char-fields

(defun atj-gen-shallow-char-fields (chars)
  (declare (xargs :guard (character-listp chars)))
  (let ((__function__ 'atj-gen-shallow-char-fields))
    (declare (ignorable __function__))
    (cond ((endp chars) nil)
          (t (cons (atj-gen-shallow-char-field (car chars))
                   (atj-gen-shallow-char-fields (cdr chars)))))))

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

(defthm jfield-listp-of-atj-gen-shallow-char-fields
  (b* ((fields (atj-gen-shallow-char-fields chars)))
    (jfield-listp fields))
  :rule-classes :rewrite)