• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
        • Deftreeops
        • Defdefparse
        • Defgrammar
        • Tree-utilities
          • Check-tree-nonleaf-num-range-4
          • Check-tree-nonleaf-num-range-3
          • Check-tree-num-range-4
          • Check-tree-nonleaf-num-range-2
          • Check-tree-num-range-3
          • Check-tree-num-range-2
          • Tree-list-tuple10
          • Check-tree-nonleaf-num-range
          • Tree-list-tuple9
          • Tree-list-tuple8
          • Tree-list-tuple7
          • Tree-list-tuple6
          • Check-tree-nonleaf-num-seq
          • Check-tree-num-range
          • Tree-list-tuple5
          • Check-tree-nonleaf-10
          • Check-tree-nonleaf-9
          • Check-tree-nonleaf-8
          • Check-tree-nonleaf-7
          • Check-tree-list-list-10
          • Tree-list-tuple4
          • Check-tree-nonleaf-6
          • Check-tree-nonleaf-5
          • Check-tree-list-list-9
          • Check-tree-nonleaf-4
          • Check-tree-nonleaf-3
          • Check-tree-nonleaf-2
          • Check-tree-nonleaf
          • Check-tree-list-list-8
          • Check-tree-nonleaf-1-1
          • Check-tree-nonleaf-1
          • Check-tree-list-list-7
          • Tree-list-tuple3
          • Pass
          • Check-tree-list-list-6
          • Check-tree-list-list-5
          • Tree=>string
          • Tree-list-tuple2
          • Check-tree-list-list-4
          • Check-tree-list-list-3
          • Check-tree-ichars
          • Check-tree-schars
          • Check-tree-num-seq
          • Check-tree-list-list-2
          • Tree-list-tuple9-result
          • Tree-list-tuple8-result
          • Tree-list-tuple7-result
          • Tree-list-tuple6-result
          • Tree-list-tuple5-result
          • Tree-list-tuple4-result
          • Tree-list-tuple3-result
          • Tree-list-tuple2-result
          • Tree-list-tuple10-result
          • Pass-result
            • Pass-result-fix
            • Pass-result-equiv
            • Pass-result-ok
            • Pass-result-err
            • Pass-resultp
              • Pass-result-kind
            • Check-tree-list-list-1
            • Tree-info-for-error
            • Check-tree-list-1
            • Check-tree-nonleaf?
            • Check-tree-leafterm
          • Notation
          • Grammar-parser
          • Meta-circular-validation
          • Parsing-primitives-defresult
          • Parsing-primitives-seq
          • Operations
          • Examples
          • Differences-with-paper
          • Constructor-utilities
          • Grammar-printer
          • Parsing-tools
        • 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
        • 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
    • Pass-result

    Pass-resultp

    Recognizer for pass-result structures.

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

    Definitions and Theorems

    Function: pass-resultp

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