		Search-engine friendly clone of the ACL2 documentation.

Values

Member-type-of-member-value

Member type of a member value.

Signature
(member-type-of-member-value member) → memtype
Arguments: member — Guard (member-valuep member).
Returns: memtype — Type (member-typep memtype).

A member-type is the static counterpart of a member-value.

Definitions and Theorems

Function: member-type-of-member-value

(defun member-type-of-member-value (member)
  (declare (xargs :guard (member-valuep member)))
  (let ((__function__ 'member-type-of-member-value))
    (declare (ignorable __function__))
    (make-member-type
         :name (member-value->name member)
         :type (type-of-value (member-value->value member)))))

Theorem: member-typep-of-member-type-of-member-value

(defthm member-typep-of-member-type-of-member-value
  (b* ((memtype (member-type-of-member-value member)))
    (member-typep memtype))
  :rule-classes :rewrite)

Theorem: member-type-of-member-value-of-member-value-fix-member

(defthm member-type-of-member-value-of-member-value-fix-member
  (equal (member-type-of-member-value (member-value-fix member))
         (member-type-of-member-value member)))

Theorem: member-type-of-member-value-member-value-equiv-congruence-on-member

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