• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
      • Std/system
        • Fresh-logical-name-with-$s-suffix
        • Irrelevant-formals-info
        • Std/system/function-queries
        • Std/system/term-queries
        • Std/system/term-transformations
          • Make-mv-let-call
          • Mvify
          • Remove-trivial-vars
          • Remove-unused-vars
          • Fsublis-fn-rec
          • Close-lambdas
          • Fsublis-var
            • Fsublis-var-lst
            • Remove-mbe-logic/exec
            • Untranslate$
            • Remove-dead-if-branches
            • Remove-progn
            • Make-mv-nth-calls
            • Apply-fn-into-ifs
            • Conjoin-equalities
            • Fapply-unary-to-terms
            • Apply-unary-to-terms
            • Apply-terms-same-args
            • Apply-term
            • Fsublis-fn-lst-simple
            • Fsublis-fn
            • Fapply-terms-same-args
            • Fsublis-fn-simple
            • Fapply-term
            • Remove-mbe-logic
            • Remove-mbe-exec
            • Quote-term
            • Quote-term-list
            • Apply-term*
            • Std/system/fsubcor-var
            • Std/system/conjoin
            • Std/system/flatten-ands-in-lit
            • Fapply-term*
            • Std/system/dumb-negate-lit
          • Std/system/enhanced-utilities
          • Install-not-normalized-event
          • Install-not-normalized-event-lst
          • Std/system/term-function-recognizers
          • Genvar$
          • Std/system/event-name-queries
          • Pseudo-tests-and-call-listp
          • Maybe-pseudo-event-formp
          • Add-suffix-to-fn-or-const
          • Chk-irrelevant-formals-ok
          • Table-alist+
          • Pseudo-tests-and-callp
          • Add-suffix-to-fn-or-const-lst
          • Known-packages+
          • Add-suffix-to-fn-lst
          • Unquote-term
          • Event-landmark-names
          • Add-suffix-lst
          • Std/system/theorem-queries
          • Unquote-term-list
          • Std/system/macro-queries
          • Pseudo-command-landmark-listp
          • Install-not-normalized$
          • Pseudo-event-landmark-listp
          • Known-packages
          • Std/system/partition-rest-and-keyword-args
          • Rune-enabledp
          • Rune-disabledp
          • Included-books
          • Std/system/pseudo-event-formp
          • Std/system/plist-worldp-with-formals
          • Std/system/w
          • Std/system/geprops
          • Std/system/arglistp
          • Std/system/constant-queries
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Fsublis-var

    Fsublis-var-lst

    Signature
    (fsublis-var-lst alist terms) → new-terms
    Arguments
    alist — Guard (and (symbol-alistp alist) (pseudo-term-listp (strip-cdrs alist))).
    terms — Guard (pseudo-term-listp terms).
    Returns
    new-terms — Type (and (pseudo-term-listp new-terms) (equal (len new-terms) (len terms))) , given the guard.