substitute into a string or a list, using eql as test
Major Section:  ACL2-BUILT-INS

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

To see the ACL2 definition of this function, see pf.