SUBST

a single substitution into a tree
Major Section:  ACL2-BUILT-INS

(Subst new old tree) is obtained by substituting new for every occurence of old in the given tree.

Equality to old is determined using the function eql. The guard for (subst new old tree) requires (eqlablep old), which ensures that the guard for eql will be met for each comparison generated by subst.

Subst is defined in Common Lisp. See any Common Lisp documentation for more information.

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