• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
          • Value-triple
          • Error-checking
          • Er
          • Assert-event
          • Error-triple
          • Set-warnings-as-errors
          • Hard-error
          • Set-inhibit-er
          • Must-fail
          • Breaks
          • Assert!-stobj
          • Ctx
          • Must-eval-to
          • Assert!
          • Must-succeed
          • Assert$
          • Illegal
          • Er-progn
          • Error1
          • Ctxp
          • Er-hard
          • Must-succeed*
          • Toggle-inhibit-er
          • Assert*
          • Assert?
          • Er-soft+
          • Er-hard?
          • Must-fail-with-soft-error
          • Must-fail-with-hard-error
          • Must-fail-with-error
          • Break$
          • Must-eval-to-t
          • Er-soft-logic
          • Er-soft
          • Convert-soft-error
            • Toggle-inhibit-er!
            • Set-inhibit-er!
            • Must-not-prove
            • Must-prove
            • Must-fail!
            • Must-be-redundant
            • Must-succeed!
            • Must-fail-local
            • Assert-equal
          • Defabbrev
          • Conses
          • 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
    • Errors

    Convert-soft-error

    Convert a soft error to have a specified (mv erp val state)

    See er for relevant background.

    General Form:
    (convert-soft-error erp val form)

    where form evaluates to an error-triple. The macro call above is equivalent to form, except that if form evaluates to (mv erp0 val0 state) where the value of erp0 is not nil and val0 is arbitrary, then erp and val are evaluated and their respective values e and v are returned in the resulting error-triple (mv erp val form). Note that it is legal for erp to have value nil, in which case that error-triple will not designate an error after all.