• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • 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
            • Concrete-syntax
            • Static-soundness
            • Static-semantics
              • Static-safety-checking
                • Check-safe-statements/blocks/cases/fundefs
                • Check-safe-expressions
                • Check-safe-fundef-list
                • Check-safe-variable-multi
                • Check-safe-variable-single
                • Check-safe-assign-multi
                • Check-safe-assign-single
                • Check-safe-path
                • Check-safe-extends-varset
                • Vars+modes
                  • Vars+modes-fix
                  • Vars+modes-equiv
                  • Make-vars+modes
                  • Vars+modes->vars
                  • Vars+modes->modes
                  • Change-vars+modes
                  • Vars+modes-p
                • Add-vars
                • Add-var
                • Add-funtypes
                • Check-safe-literal
                • Funtype
                • Get-funtype
                • Check-var
                • Check-safe-top-block
                • Check-safe-path-list
                • Vars+modes-result
                • Funtype-result
                • Funtable-result
                • Funtable-for-fundefs
                • Funtype-for-fundef
                • Funtable
              • Static-shadowing-checking
              • Mode-set-result
              • Literal-evaluation
              • Static-identifier-checking
              • Static-safety-checking-evm
              • Mode-set
              • Modes
            • 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
  • Static-safety-checking

Vars+modes

Fixtype of pairs consisting of a variable table and a set of modes.

This is a product type introduced by fty::defprod.

Fields
vars — identifier-set
modes — mode-set

Values of this fixtype capture the information calculated by the successful check of statements. The variable table captures the updated variable table. The set of modes captures the possible ways in which the statement may terminate.

Subtopics

Vars+modes-fix
Fixing function for vars+modes structures.
Vars+modes-equiv
Basic equivalence relation for vars+modes structures.
Make-vars+modes
Basic constructor macro for vars+modes structures.
Vars+modes->vars
Get the vars field from a vars+modes.
Vars+modes->modes
Get the modes field from a vars+modes.
Change-vars+modes
Modifying constructor for vars+modes structures.
Vars+modes-p
Recognizer for vars+modes structures.