		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Lhsarr-fix

Signature
(lhsarr-fix lhsarr) → lhsarr

Definitions and Theorems

Function: lhsarr-fix$inline

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