		Search-engine friendly clone of the ACL2 documentation.

Alias-norm.lisp

Aliases-empty

Signature
(aliases-empty aliases) → aliases

Definitions and Theorems

Function: aliases-empty

(defun aliases-empty (aliases)
  (declare (xargs :stobjs (aliases)))
  (declare (xargs :guard t))
  (let ((__function__ 'aliases-empty))
    (declare (ignorable __function__))
    (mbe :logic (non-exec nil)
         :exec (resize-aliass 0 aliases))))