		Search-engine friendly clone of the ACL2 documentation.

Values

Init-type-of-init-value

Initialization type of an initialization value.

Signature
(init-type-of-init-value ival) → itype
Arguments: ival — Guard (init-valuep ival).
Returns: itype — Type (init-typep itype).

An init-type is the static counterpart of an init-value.

Definitions and Theorems

Function: init-type-of-init-value

(defun init-type-of-init-value (ival)
 (declare (xargs :guard (init-valuep ival)))
 (let ((__function__ 'init-type-of-init-value))
   (declare (ignorable __function__))
   (init-value-case
        ival
        :single (init-type-single (type-of-value ival.get))
        :list (init-type-list (type-list-of-value-list ival.get)))))

Theorem: init-typep-of-init-type-of-init-value

(defthm init-typep-of-init-type-of-init-value
  (b* ((itype (init-type-of-init-value ival)))
    (init-typep itype))
  :rule-classes :rewrite)

Theorem: init-type-of-init-value-of-init-value-fix-ival

(defthm init-type-of-init-value-of-init-value-fix-ival
  (equal (init-type-of-init-value (init-value-fix ival))
         (init-type-of-init-value ival)))

Theorem: init-type-of-init-value-init-value-equiv-congruence-on-ival

(defthm init-type-of-init-value-init-value-equiv-congruence-on-ival
  (implies (init-value-equiv ival ival-equiv)
           (equal (init-type-of-init-value ival)
                  (init-type-of-init-value ival-equiv)))
  :rule-classes :congruence)