• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Miscellaneous
      • Output-controls
      • Bdd
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
          • Convert-subexpression-to-mv
          • Ute-term-p
          • Reincarnate-mvs
            • Reincarnate-mvs-list
            • Match-cons-nest
          • Macro-libraries
          • Add-macro-fn
          • Check-vars-not-free
          • Safe-mode
          • Trans1
          • Defmacro-untouchable
          • Set-duplicate-keys-action
          • Add-macro-alias
          • Magic-macroexpand
          • Defmacroq
          • Trans!
          • Remove-macro-fn
          • Remove-macro-alias
          • Add-binop
          • Untrans-table
          • Trans*-
          • Remove-binop
          • Tcp
          • Tca
        • Installation
        • Mailing-lists
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Reincarnate-mvs

    Reincarnate-mvs-list

    Signature
    (reincarnate-mvs-list x world) → (mv errmsg new-x)
    Arguments
    x — The terms to try to untranslate.
        Guard (ute-termlist-p x).
    world — The world, needed for stobjs-out lookups.
        Guard (plist-worldp world).
    Returns
    errmsg — NIL on success or an error msg on failure.
    new-x — New version of x with MVs restored.
        Type (and (implies (ute-termlist-p x) (ute-termlist-p new-x)) (equal (len new-x) (len x))) .