|
|
|---|
|
|
|
|---|
Fixtype of (ATC's model of) arrays of type
This is a product type introduced by fty::defprod.
The following invariant is enforced on the fields:
(and (type-case elemtype :schar) (consp elements))
Theorem:
(defthm schar-arrayp-alt-def (equal (schar-arrayp x) (and (valuep x) (value-case x :array) (equal (value-array->elemtype x) (type-schar)) (schar-listp (value-array->elements x)))))
Theorem:
(defthm schar-array->elements-alt-def (implies (schar-arrayp array) (equal (schar-array->elements array) (value-array->elements array))))