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.
