Major Section: ACL2-BUILT-INS
(Subst new old tree) is obtained by substituting
new for every
old in the given tree.
old is determined using the function
(subst new old tree) requires
(eqlablep old), which
ensures that the guard for
eql will be met for each comparison
Subst is defined in Common Lisp. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.