		Search-engine friendly clone of the ACL2 documentation.

Desiniter

Desiniter->initer

Get the initer field from a desiniter.

Signature
(desiniter->initer x) → initer
Arguments: x — Guard (desiniterp x).
Returns: initer — Type (initerp initer).

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

Definitions and Theorems

Function: desiniter->initer$inline

(defun desiniter->initer$inline (x)
  (declare (xargs :guard (desiniterp x)))
  (declare (xargs :guard t))
  (mbe :logic
       (b* ((x (and t x)))
         (initer-fix (cdr x)))
       :exec (cdr x)))

Theorem: initerp-of-desiniter->initer

(defthm initerp-of-desiniter->initer
  (b* ((initer (desiniter->initer$inline x)))
    (initerp initer))
  :rule-classes :rewrite)

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

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

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

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