SUBSTITUTE

substitute into a string or a list, using eql as test
Major Section:  PROGRAMMING

(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.