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
alist. However, a leaf is left unchanged if it is not found
as a key in
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 is defined in Common Lisp. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.