		Search-engine friendly clone of the ACL2 documentation.

Desiniter

Desiniter->designors

Get the designors field from a desiniter.

Signature
(desiniter->designors x) → designors
Arguments: x — Guard (desiniterp x).
Returns: designors — Type (designor-listp designors).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: desiniter->designors$inline

(defun desiniter->designors$inline (x)
  (declare (xargs :guard (desiniterp x)))
  (declare (xargs :guard t))
  (mbe :logic
       (b* ((x (and t x)))
         (designor-list-fix (car x)))
       :exec (car x)))

Theorem: designor-listp-of-desiniter->designors

(defthm designor-listp-of-desiniter->designors
  (b* ((designors (desiniter->designors$inline x)))
    (designor-listp designors))
  :rule-classes :rewrite)

Theorem: desiniter->designors$inline-of-desiniter-fix-x

(defthm desiniter->designors$inline-of-desiniter-fix-x
  (equal (desiniter->designors$inline (desiniter-fix x))
         (desiniter->designors$inline x)))

Theorem: desiniter->designors$inline-desiniter-equiv-congruence-on-x

(defthm desiniter->designors$inline-desiniter-equiv-congruence-on-x
  (implies (desiniter-equiv x x-equiv)
           (equal (desiniter->designors$inline x)
                  (desiniter->designors$inline x-equiv)))
  :rule-classes :congruence)