SUBLIS

substitute an alist into a tree
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.