Vl-ps->chars
(vl-ps->chars) returns what was printed as a character list in
the proper, non-reversed, printed order.
- Signature
(vl-ps->chars &key (ps 'ps)) → chars
- Returns
- chars — Type (character-listp chars).
This is expensive. It necessarily involves creating n conses,
where n is the number of characters printed. If you really want a string,
vl-ps->string will be faster.
Definitions and Theorems
Function: vl-ps->chars-fn
(defun vl-ps->chars-fn (ps)
(declare (xargs :stobjs (ps)))
(declare (xargs :guard t))
(let ((__function__ 'vl-ps->chars))
(declare (ignorable __function__))
(vl-printedlist->chars (vl-ps->rchars)
nil)))
Theorem: character-listp-of-vl-ps->chars
(defthm character-listp-of-vl-ps->chars
(b* ((chars (vl-ps->chars-fn ps)))
(character-listp chars))
:rule-classes :rewrite)
Subtopics
- Vl-printedlist->chars
- Convert a printed list (in reverse order) into characters (in proper
order).
