|
|
|---|
|
|
|
|---|
Get the length of the obs-sdom-array array.
In the execution this just gets the array length. The logical definition is just a wrapper for len:
Function:
(defun sdominfos$a-length (obs-sdom-array$a) (declare (xargs :guard (obs-sdom-array$ap obs-sdom-array$a))) (len obs-sdom-array$a))