		Search-engine friendly clone of the ACL2 documentation.

Alias-norm.lisp

Aliases-fix

Signature
(aliases-fix aliases) → aliases

Definitions and Theorems

Function: aliases-fix$inline

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