		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-pos-isomap-alist-stobjp

Check if at least one conversion in one isomorphic mapping in the alist from positive integers to isomorphic mappings has input or output stobjs.

Signature
(isodata-pos-isomap-alist-stobjp alist) → yes/no
Arguments: alist — Guard (isodata-pos-isomap-alistp alist).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: isodata-pos-isomap-alist-stobjp

(defun isodata-pos-isomap-alist-stobjp (alist)
  (declare (xargs :guard (isodata-pos-isomap-alistp alist)))
  (let ((__function__ 'isodata-pos-isomap-alist-stobjp))
    (declare (ignorable __function__))
    (and (mbt (isodata-pos-isomap-alistp alist))
         (not (endp alist))
         (or (isodata-isomap->stobjp (cdar alist))
             (isodata-pos-isomap-alist-stobjp (cdr alist))))))

Theorem: booleanp-of-isodata-pos-isomap-alist-stobjp

(defthm booleanp-of-isodata-pos-isomap-alist-stobjp
  (b* ((yes/no (isodata-pos-isomap-alist-stobjp alist)))
    (booleanp yes/no))
  :rule-classes :rewrite)