Build an array of type
(ullong-array-of elements) → array
Function:
(defun ullong-array-of (elements) (declare (xargs :guard (ullong-listp elements))) (declare (xargs :guard (consp elements))) (let ((__function__ 'ullong-array-of)) (declare (ignorable __function__)) (ullong-array (type-ullong) elements)))
Theorem:
(defthm ullong-arrayp-of-ullong-array-of (b* ((array (ullong-array-of elements))) (ullong-arrayp array)) :rule-classes :rewrite)
Theorem:
(defthm ullong-array-of-of-ullong-array->elements (equal (ullong-array-of (ullong-array->elements array)) (ullong-array-fix array)))
Theorem:
(defthm ullong-array-of-alt-def (implies (and (ullong-listp elems) (consp elems)) (equal (ullong-array-of elems) (make-value-array :elemtype (type-ullong) :elements elems))))
Theorem:
(defthm ullong-array-of-of-ullong-list-fix-elements (equal (ullong-array-of (ullong-list-fix elements)) (ullong-array-of elements)))
Theorem:
(defthm ullong-array-of-ullong-list-equiv-congruence-on-elements (implies (ullong-list-equiv elements elements-equiv) (equal (ullong-array-of elements) (ullong-array-of elements-equiv))) :rule-classes :congruence)