• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
          • Transformations
          • Language
            • Abstract-syntax
            • Dynamic-semantics
              • Exec
                • Exec-statement
                • Exec-function
                • Exec-for-iterations
                • Exec-block
                • Exec-switch-rest
                • Exec-expression-list
                  • Exec-funcall
                  • Exec-statement-list
                  • Exec-expression
                • Find-fun
                • Init-local
                • Write-vars-values
                • Add-vars-values
                • Add-funs
                • Eoutcome
                • Soutcome
                • Ensure-funscope-disjoint
                • Write-var-value
                • Restrict-vars
                • Add-var-value
                • Funinfo
                • Exec-top-block
                • Values
                • Cstate
                • Funinfo+funenv
                • Read-vars-values
                • Read-var-value
                • Funenv
                • Funscope-for-fundefs
                • Exec-path
                • Path-to-var
                • Funinfo+funenv-result
                • Exec-literal
                • Soutcome-result
                • Mode-set-result
                • Literal-evaluation
                • Funscope-result
                • Funinfo-result
                • Funenv-result
                • Eoutcome-result
                • Cstate-result
                • Paths-to-vars
                • Funinfo-for-fundef
                • Lstate
                • Funscope
                • Mode-set
                • Modes
              • Concrete-syntax
              • Static-soundness
              • Static-semantics
              • Errors
            • Yul-json
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Exec

    Exec-expression-list

    Execute a list of expressions.

    Signature
    (exec-expression-list exprs cstate funenv limit) → outcome
    Arguments
    exprs — Guard (expression-listp exprs).
    cstate — Guard (cstatep cstate).
    funenv — Guard (funenvp funenv).
    limit — Guard (natp limit).
    Returns
    outcome — Type (eoutcome-resultp outcome).

    Lists of expressions are evaluated left-to-right. Lists of expressions are used as arguments of function calls. Each expression in the list must return exactly one result. The returned expression outcome, if all the expressions are successfuly evaluated, includes a list of values, one for each expression, in the same order.