• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Mutual-recursion
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Loop$-primer
        • Fast-alists
        • Defmacro
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • Developers-guide
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Numbers
        • Irrelevant-formals
        • Efficiency
        • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
        • Redefining-programs
        • Lists
        • Invariant-risk
        • Errors
        • Defabbrev
        • Conses
          • Cdr
          • Car
          • Cons
          • Consp
          • Cons-with-hint
          • Atom
          • Subst
            • Cadr
            • Listp
            • Cons-count-bounded
            • Cddr
            • Caar
            • Caddr
            • Cdddr
            • Cddar
            • Cdar
            • Cdadr
            • Cdaar
            • Cadar
            • Caadr
            • Caaar
            • Cadddr
            • Caddar
            • Cddddr
            • Cdddar
            • Cddadr
            • Cddaar
            • Cdaddr
            • Cdadar
            • Cdaadr
            • Cdaaar
            • Cadadr
            • Cadaar
            • Caaddr
            • Caadar
            • Caaadr
            • Caaaar
          • Alists
          • Set-register-invariant-risk
          • Strings
          • Program-wrapper
          • Get-internal-time
          • Basics
          • Packages
          • Defmacro-untouchable
          • Primitive
          • <<
          • Revert-world
          • Set-duplicate-keys-action
          • Unmemoize
          • Symbols
          • Def-list-constructor
          • Easy-simplify-term
          • Defiteration
          • Defopen
          • Sleep
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Conses
    • ACL2-built-ins

    Subst

    A single substitution into a tree

    (Subst new old tree) is obtained by substituting new for every occurrence 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.

    Function: subst

    (defun subst (new old tree)
           (declare (xargs :guard (eqlablep old)))
           (cond ((eql old tree) new)
                 ((atom tree) tree)
                 (t (cons (subst new old (car tree))
                          (subst new old (cdr tree))))))