• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • Macro-libraries
          • B*
            • B*-binders
              • ACL2::patbind-ret
              • ACL2::patbind-stobj-get
              • Patbind-match
              • Patbind-when
              • Patbind-assocs
              • Patbind-the
              • Patbind-nths*
              • Patbind-er
              • Patbind-nths
              • Patbind-macro
              • Patbind-fun
              • Patbind-faig
              • Patbind-run-when
              • Patbind-pattern
              • Patbind-mv
              • Patbind-list*
              • Patbind-list
              • Patbind-cmp
              • Patbind-with-stolen
              • Patbind-with-fast
              • Patbind-unless-casematch
              • Patbind-cons
              • Patbind-access
              • Patbind-extract-keyword-args
              • Patbind-run-unless
              • Patbind-free-on-exit
              • Patbind-unless
              • Patbind-local-stobjs
              • Patbind-if
              • Patbind-getargs
              • Patbind-run-if
              • Patbind-state-global
                • Patbind-vl-read-zip-header-ret
                • Patbind-test-glmc-interp-nonhyps-ret
                • Patbind-test-glmc-interp-hyps-ret
                • Patbind-glmc-generic-interp-nonhyps-ret
                • Patbind-glmc-generic-interp-hyps-ret
              • Def-b*-binder
            • Defunc
            • Fty
            • Apt
            • Std/util
            • Defdata
            • Defrstobj
            • Seq
            • Match-tree
            • Defrstobj
            • With-supporters
            • Def-partial-measure
            • Template-subst
            • Soft
            • Defthm-domain
            • Event-macros
            • Def-universal-equiv
            • Def-saved-obligs
            • With-supporters-after
            • Definec
            • Sig
            • Outer-local
            • Data-structures
          • 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
        • Mailing-lists
        • Interfacing-tools
      • Macro-libraries
        • B*
          • B*-binders
            • ACL2::patbind-ret
            • ACL2::patbind-stobj-get
            • Patbind-match
            • Patbind-when
            • Patbind-assocs
            • Patbind-the
            • Patbind-nths*
            • Patbind-er
            • Patbind-nths
            • Patbind-macro
            • Patbind-fun
            • Patbind-faig
            • Patbind-run-when
            • Patbind-pattern
            • Patbind-mv
            • Patbind-list*
            • Patbind-list
            • Patbind-cmp
            • Patbind-with-stolen
            • Patbind-with-fast
            • Patbind-unless-casematch
            • Patbind-cons
            • Patbind-access
            • Patbind-extract-keyword-args
            • Patbind-run-unless
            • Patbind-free-on-exit
            • Patbind-unless
            • Patbind-local-stobjs
            • Patbind-if
            • Patbind-getargs
            • Patbind-run-if
            • Patbind-state-global
              • Patbind-vl-read-zip-header-ret
              • Patbind-test-glmc-interp-nonhyps-ret
              • Patbind-test-glmc-interp-hyps-ret
              • Patbind-glmc-generic-interp-nonhyps-ret
              • Patbind-glmc-generic-interp-hyps-ret
            • Def-b*-binder
          • Defunc
          • Fty
          • Apt
          • Std/util
          • Defdata
          • Defrstobj
          • Seq
          • Match-tree
          • Defrstobj
          • With-supporters
          • Def-partial-measure
          • Template-subst
          • Soft
          • Defthm-domain
          • Event-macros
          • Def-universal-equiv
          • Def-saved-obligs
          • With-supporters-after
          • Definec
          • Sig
          • Outer-local
          • Data-structures
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • B*-binders

      Patbind-state-global

      b* binder for accessing state globals.

      Usage:

      (b* (((state-global x) (value-form)))
        (result-form))

      is equivalent to

      (state-global-let* ((x (value-form)))
        (result-form))