• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
            • Exec
            • 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
              • Funscope-result-fix
              • Funscope-result-equiv
              • Funscope-result-ok
              • Funscope-result-err
              • Funscope-resultp
                • Funscope-result-kind
              • 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
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Funscope-result

    Funscope-resultp

    Recognizer for funscope-result structures.

    Signature
    (funscope-resultp acl2::x) → *

    Definitions and Theorems

    Function: funscope-resultp

    (defun funscope-resultp (acl2::x)
      (declare (xargs :guard t))
      (let ((__function__ 'funscope-resultp))
        (declare (ignorable __function__))
        (cond ((funscopep acl2::x)
               (b* ((get acl2::x)) (funscopep get)))
              (t (b* ((get acl2::x)) (reserrp get))))))