Major Section: ACL2-BUILT-INS
(Sublis alist tree) is obtained by replacing every leaf of
tree with the result of looking that leaf up in the association
list alist. However, a leaf is left unchanged if it is not found
as a key in alist.
Leaves are looked up using the function assoc. The guard for
(sublis alist tree) requires (eqlable-alistp alist). This
guard ensures that the guard for assoc will be met for each
lookup generated by sublis.
Sublis is defined in Common Lisp. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.
