		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svexarr-fix

Signature
(svexarr-fix svexarr) → svexarr

Definitions and Theorems

Function: svexarr-fix$inline

(defun svexarr-fix$inline (svexarr)
  (declare (xargs :stobjs (svexarr)))
  (declare (xargs :guard t))
  (let ((__function__ 'svexarr-fix))
    (declare (ignorable __function__))
    (mbe :logic (non-exec (svexlist-fix svexarr))
         :exec svexarr)))