Collect-aliases
- Signature
(collect-aliases n aliases) → *
- Arguments
- n — Guard (natp n).
Definitions and Theorems
Function: collect-aliases
(defun collect-aliases (n aliases)
(declare (xargs :stobjs (aliases)))
(declare (xargs :guard (natp n)))
(declare (xargs :guard (<= n (aliass-length aliases))))
(let ((__function__ 'collect-aliases))
(declare (ignorable __function__))
(b* (((when (mbe :logic (zp (- (aliass-length aliases) (nfix n)))
:exec (eql n (aliass-length aliases))))
nil))
(cons (get-alias n aliases)
(collect-aliases (1+ (lnfix n))
aliases)))))
