Convert array type to pointer type.
Under most circumstances, an array is converted to a pointer to the first element of the array [C:6.3.2.1/3]; indeed, arrays are used like pointers most of the time.
This conversion is captured, at the level of types, here. Non-array types are left unchanged.
The dynamic counterpart of this is apconvert-expr-value.
Function:
(defun apconvert-type (type) (declare (xargs :guard (typep type))) (let ((__function__ 'apconvert-type)) (declare (ignorable __function__)) (if (type-case type :array) (type-pointer (type-array->of type)) (type-fix type))))
Theorem:
(defthm typep-of-apconvert-type (b* ((type1 (apconvert-type type))) (typep type1)) :rule-classes :rewrite)
Theorem:
(defthm type-arithmeticp-of-apconvert-type (equal (type-arithmeticp (apconvert-type type)) (type-arithmeticp type)))
Theorem:
(defthm apconvert-type-of-type-fix-type (equal (apconvert-type (type-fix type)) (apconvert-type type)))
Theorem:
(defthm apconvert-type-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (apconvert-type type) (apconvert-type type-equiv))) :rule-classes :congruence)