Substitute
Substitute into a string or a list, using eql as test
(Substitute new old seq) is the result of replacing each
occurrence of old in seq, which is a list or a string, with
new.
The guard for substitute requires that either seq is a string and
new is a character, or else: seq is a true-listp such that
either all of its members are eqlablep or old is
eqlablep.
Substitute is a Common Lisp function. See any Common Lisp
documentation for more information. Since ACL2 functions cannot take keyword
arguments (though macros can), the test used in substitute is
eql.
Function: substitute
(defun substitute (new old seq)
(declare (xargs :guard (or (and (stringp seq) (characterp new))
(and (true-listp seq)
(or (eqlablep old)
(eqlable-listp seq))))))
(if (stringp seq)
(coerce (substitute-ac new old (coerce seq 'list)
nil)
'string)
(substitute-ac new old seq nil)))Subtopics
- Strsubst
- Replace substrings throughout a string.
