		Search-engine friendly clone of the ACL2 documentation.

Omaps

Mapp

Recognize omaps.

Signature
(mapp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

This is similar to the definition of setp, but each element of the list is checked to be a cons pair and the ordering comparison is performed on the cars.

Definitions and Theorems

Function: mapp

(defun mapp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'mapp))
    (declare (ignorable __function__))
    (if (atom x)
        (null x)
      (and (consp (car x))
           (or (null (cdr x))
               (and (consp (cdr x))
                    (consp (cadr x))
                    (fast-<< (caar x) (caadr x))
                    (mapp (cdr x))))))))

Theorem: booleanp-of-mapp

(defthm booleanp-of-mapp
  (b* ((yes/no (mapp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: setp-when-mapp

(defthm setp-when-mapp
  (implies (mapp x) (setp x))
  :rule-classes (:rewrite :forward-chaining))

Theorem: alistp-when-mapp

(defthm alistp-when-mapp
  (implies (mapp x) (alistp x))
  :rule-classes (:rewrite :forward-chaining))