• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • 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
            • Aliases-indexed->named-aux
            • Svex-compose-assigns/delays
            • 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
            • 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
            • Aliases-boundedp-aux
            • Svex-apply-overrides
            • Indnamememo-to-var-decl-map
            • Indname-result
            • Assigns-compose
            • Delay-svarlist->delays
            • Indnamememo
            • Svex-override-vars
            • Delay-svar->delays
            • Assigns-to-overrides
            • Svarlist-collect-delays
            • Svex-overridelist-vars
            • Svex-overridelist-keys
            • Assigns-to-overrides-nrev
            • Var-decl-map
            • Cap-length
          • Assign->segment-drivers
          • Segment-driver-map-resolve
          • Assigns->segment-drivers
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Compile.lisp

Maybe-indname-result

Option type; indname-result or nil.

This is an option type introduced by fty::defoption. Note that defoption is just a wrapper for defflexsum, so there are :none and :some member types, a case macro, and so forth.

Member Types
:none → maybe-indname-result-none
Represents that no maybe-indname-result is available, i.e., Nothing or None.
:some → maybe-indname-result-some
An available maybe-indname-result, i.e., Just val or Some val.

Subtopics

Maybe-indname-result-fix
Fixing function for maybe-indname-result structures.
Maybe-indname-result-equiv
Basic equivalence relation for maybe-indname-result structures.
Maybe-indname-result-case
Case macro for the different kinds of maybe-indname-result structures.
Maybe-indname-result-some
An available maybe-indname-result, i.e., Just val or Some val.
Maybe-indname-result-none
Represents that no maybe-indname-result is available, i.e., Nothing or None.
Maybe-indname-result-p
Recognizer for maybe-indname-result structures.