• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
          • World
          • Io
          • Wormhole
          • Programming-with-state
            • Error-triple
            • Cbd
            • State-global-let*
            • Last-prover-steps
            • @
            • Assign
            • Read-run-time
            • Canonical-pathname
            • F-put-global
            • Unsound-eval
            • Setenv$
            • Er-progn
              • Read-ACL2-oracle
              • With-live-state
              • F-get-global
              • Getenv$
              • Pprogn
              • Get-real-time
              • Makunbound-global
              • Get-cpu-time
              • F-boundp-global
              • Probe-file
            • W
            • Set-state-ok
            • Random$
          • Mutual-recursion
          • Memoize
          • Mbe
          • Io
          • Defpkg
          • Apply$
          • Loop$
          • Programming-with-state
            • Error-triple
            • Cbd
            • State-global-let*
            • Last-prover-steps
            • @
            • Assign
            • Read-run-time
            • Canonical-pathname
            • F-put-global
            • Unsound-eval
            • Setenv$
            • Er-progn
              • Read-ACL2-oracle
              • With-live-state
              • F-get-global
              • Getenv$
              • Pprogn
              • Get-real-time
              • Makunbound-global
              • Get-cpu-time
              • F-boundp-global
              • Probe-file
            • Arrays
            • Characters
            • Time$
            • Defmacro
            • Loop$-primer
            • Fast-alists
            • Defconst
            • Evaluation
            • Guard
            • Equality-variants
            • Compilation
            • Hons
            • ACL2-built-ins
            • Developers-guide
            • System-attachments
            • Advanced-features
            • Set-check-invariant-risk
            • Numbers
            • Efficiency
            • Irrelevant-formals
            • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
            • Redefining-programs
            • Lists
            • Invariant-risk
            • Errors
            • Defabbrev
            • Conses
            • Alists
            • Set-register-invariant-risk
            • Strings
            • Program-wrapper
            • Get-internal-time
            • Basics
            • Packages
            • Oracle-eval
            • Defmacro-untouchable
            • <<
            • Primitive
            • Revert-world
            • Unmemoize
            • Set-duplicate-keys-action
            • Symbols
            • Def-list-constructor
            • Easy-simplify-term
            • Defiteration
            • Fake-oracle-eval
            • Defopen
            • Sleep
          • Operational-semantics
          • Real
          • Start-here
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Errors
      • Programming-with-state
      • ACL2-built-ins

      Er-progn

      Perform a sequence of state-changing ``error triples''

      Example:
      (er-progn (check-good-foo-p (f-get-global 'my-foo state) state)
                (value (* (f-get-global 'my-foo state)
                          (f-get-global 'bar state))))

      This sequencing primitive is only useful when programming with state, something that very few users will probably want to do. See state.

      Er-progn is used much the way that progn is used in Common Lisp, except that it expects each form within it to evaluate to an error-triple of the form (mv erp val state). The first such form, if any, that evaluates to such a triple where erp is not nil yields the error triple returned by the er-progn. If there is no such form, then the er-progn form returns the value of the last form.

      General Form:
      (er-progn <expr1> ... <exprk>)

      where each <expri> is an expression that evaluates to an error triple (see programming-with-state). The above form is essentially equivalent to the following (``essentially'' because in fact, care is taken to avoid variable capture).

      (mv-let (erp val state)
              <expr1>
              (cond (erp (mv erp val state))
                    (t (mv-let (erp val state)
                               <expr2>
                               (cond (erp (mv erp val state))
                                     (t ...
                                            (mv-let (erp val state)
                                                    <expr{k-1}>
                                                    (cond (erp (mv erp val state))
                                                          (t <exprk>)))))))))