• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-fixpoint-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Moddb
        • Svex-compilation
          • Alias-normalization
          • Svex-design-flatten-and-normalize
          • Svex-design-compile
          • Svex-composition
          • Compile.lisp
            • Svex-normalize-assigns
            • Svex-design-flatten
            • Svex-override-lhrange
            • Svex-override-lhs
            • Svex-compose-assigns/delays
            • Aliases-indexed->named-aux
            • Svex-alist-truncate-by-var-decls
            • Svar-map-truncate-by-var-decls
            • Aliases-to-var-decl-map-aux
            • Aliases-indexed->named
            • Svar-indexed->named-memo
            • Lhs-indexed->named
            • Maybe-svar-p
            • Svar-register-indnamememo
            • Svarlist-indexed->named
            • Maybe-svar-fix
            • Lhs-register-indnamememo
            • Maybe-indname-result
              • Maybe-indname-result-fix
              • Maybe-indname-result-equiv
              • Maybe-indname-result-case
              • Maybe-indname-result-some
              • Maybe-indname-result-none
              • Maybe-indname-result-p
              • Aliases-to-var-decl-map
              • Svar-indexed->named
              • Svex-apply-overrides
              • Aliases-boundedp-aux
              • Indnamememo-to-var-decl-map
              • Indname-result
              • Assigns-compose
              • Delay-svarlist->delays
              • Svex-override-vars
              • Indnamememo
              • Delay-svar->delays
              • Assigns-to-overrides
              • Svarlist-collect-delays
              • Svex-overridelist-vars
              • Svex-overridelist-keys
              • Assigns-to-overrides-nrev
              • Cap-length
              • Var-decl-map
            • Assign->netassigns
          • Svmods
          • Svstmt
          • Sv-tutorial
          • Expressions
          • Symbolic-test-vector
          • Vl-to-svex
        • Vwsim
        • Fgl
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Testing-utilities
      • Math
    • Maybe-indname-result

    Maybe-indname-result-p

    Recognizer for maybe-indname-result structures.

    Signature
    (maybe-indname-result-p x) → *

    Definitions and Theorems

    Function: maybe-indname-result-p

    (defun maybe-indname-result-p (x)
           (declare (xargs :guard t))
           (let ((__function__ 'maybe-indname-result-p))
                (declare (ignorable __function__))
                (cond ((not x) (b* nil t))
                      (t (b* ((fty::val x))
                             (indname-result-p fty::val))))))