		Search-engine friendly clone of the ACL2 documentation.

Type

Type-count

Measure for recurring over type structures.

Signature
(type-count x) → count
Arguments: x — Guard (typep x).
Returns: count — Type (natp count).

Definitions and Theorems

Function: type-count

(defun type-count (x)
  (declare (xargs :guard (typep x)))
  (case (type-kind x)
    (:void 1)
    (:char 1)
    (:schar 1)
    (:uchar 1)
    (:sshort 1)
    (:ushort 1)
    (:sint 1)
    (:uint 1)
    (:slong 1)
    (:ulong 1)
    (:sllong 1)
    (:ullong 1)
    (:struct 1)
    (:pointer (+ 2 (type-count (type-pointer->to x))))
    (:array (+ 3 (type-count (type-array->of x))))))

Theorem: natp-of-type-count

(defthm natp-of-type-count
  (b* ((count (type-count x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: type-count-of-type-fix-x

(defthm type-count-of-type-fix-x
  (equal (type-count (type-fix x))
         (type-count x)))

Theorem: type-count-type-equiv-congruence-on-x

(defthm type-count-type-equiv-congruence-on-x
  (implies (type-equiv x x-equiv)
           (equal (type-count x)
                  (type-count x-equiv)))
  :rule-classes :congruence)

Theorem: type-count-of-type-pointer

(defthm type-count-of-type-pointer
  (implies t
           (< (+ (type-count to))
              (type-count (type-pointer to))))
  :rule-classes :linear)

Theorem: type-count-of-type-pointer->to

(defthm type-count-of-type-pointer->to
  (implies (equal (type-kind x) :pointer)
           (< (type-count (type-pointer->to x))
              (type-count x)))
  :rule-classes :linear)

Theorem: type-count-of-type-array

(defthm type-count-of-type-array
  (implies t
           (< (+ (type-count of))
              (type-count (type-array of size))))
  :rule-classes :linear)

Theorem: type-count-of-type-array->of

(defthm type-count-of-type-array->of
  (implies (equal (type-kind x) :array)
           (< (type-count (type-array->of x))
              (type-count x)))
  :rule-classes :linear)