• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
          • Defbyte
          • Defresult
          • Fold
          • Specific-types
            • Pos-list
            • Defbyte-standard-instances
            • Defbytelist-standard-instances
            • Byte-list
            • Byte
            • String-option
            • Pos-option
            • Nibble
            • Nat-option
            • Ubyte32-option
            • Byte-list20
            • Byte-list32
            • Byte-list64
            • Pseudo-event-form
            • Natoption/natoptionlist
              • Natoption/natoptionlist-fix
              • Natoption/natoptionlist-case
                • Natoption/natoptionlist-equiv
                • Natoption/natoptionlist-p
                • Natoption/natoptionlist-one
                • Natoption/natoptionlist-list
                • Natoption/natoptionlist-kind
              • Nati
              • Character-list
              • Nat/natlist
              • Maybe-string
              • Nibble-list
              • Natoption/natoptionlist-result
              • Nat/natlist-result
              • Nat-option-list-result
              • Set
              • String-result
              • String-list-result
              • Nat-result
              • Nat-option-result
              • Nat-list-result
              • Maybe-string-result
              • Integer-result
              • Character-result
              • Character-list-result
              • Boolean-result
              • Map
              • Bag
              • Pos-set
              • Hex-digit-char-list
              • Dec-digit-char-list
              • Pseudo-event-form-list
              • Nat-option-list
              • Character-any-map
              • Any-nat-map
              • Symbol-set
              • String-set
              • Nat-set
              • Character-set
              • Oct-digit-char-list
              • Bin-digit-char-list
              • Bit-list
            • Defsubtype
            • Defset
            • Defflatsum
            • Deflist-of-len
            • Pos-list
            • Defomap
            • Defbytelist
            • Defbyte-standard-instances
            • Deffixtype-alias
            • Defbytelist-standard-instances
            • Defunit
            • Byte-list
            • Database
            • Byte
            • String-option
            • Pos-option
            • Nibble
            • Nat-option
            • Ubyte32-option
            • Byte-list20
            • Byte-list32
            • Byte-list64
            • Pseudo-event-form
            • Natoption/natoptionlist
              • Natoption/natoptionlist-fix
              • Natoption/natoptionlist-case
                • Natoption/natoptionlist-equiv
                • Natoption/natoptionlist-p
                • Natoption/natoptionlist-one
                • Natoption/natoptionlist-list
                • Natoption/natoptionlist-kind
              • Nati
              • Character-list
              • Nat/natlist
              • Maybe-string
              • Nibble-list
              • Natoption/natoptionlist-result
              • Nat/natlist-result
              • Nat-option-list-result
              • Set
              • String-result
              • String-list-result
              • Nat-result
              • Nat-option-result
              • Nat-list-result
              • Maybe-string-result
              • Integer-result
              • Character-result
              • Character-list-result
              • Boolean-result
              • Map
              • Dependencies
              • Bag
              • Pos-set
              • Hex-digit-char-list
              • Dec-digit-char-list
              • Pseudo-event-form-list
              • Nat-option-list
              • Character-any-map
              • Any-nat-map
              • Symbol-set
              • String-set
              • Nat-set
              • Character-set
              • Oct-digit-char-list
              • Bin-digit-char-list
              • Bit-list
            • Isar
            • Kestrel-utilities
            • Set
            • C
            • Soft
            • Bv
            • Imp-language
            • Ethereum
            • Event-macros
            • Java
            • Riscv
            • Bitcoin
            • Zcash
            • Yul
            • ACL2-programming-language
            • Prime-fields
            • Json
            • Syntheto
            • File-io-light
            • Cryptography
            • Number-theory
            • Axe
            • Lists-light
            • Builtins
            • Solidity
            • Helpers
            • Htclient
            • Typed-lists-light
            • Arithmetic-light
          • X86isa
          • Axe
          • Execloader
        • Math
        • Testing-utilities
      • Natoption/natoptionlist

      Natoption/natoptionlist-case

      Case macro for the different kinds of natoption/natoptionlist structures.

      This is an fty sum-type case macro, typically introduced by fty::defflexsum or fty::deftagsum. It allows you to safely check the type of a natoption/natoptionlist structure, or to split into cases based on its type.

      Short Form

      In its short form, natoption/natoptionlist-case allows you to safely check the type of a natoption/natoptionlist structure. For example:

      (natoption/natoptionlist-case x :one)

      is essentially just a safer alternative to writing:

      (equal (natoption/natoptionlist-kind x) :one)

      Why is using natoption/natoptionlist-case safer? When we directly inspect the kind with equal, there is no static checking being done to ensure that, e.g., :one is a valid kind of natoption/natoptionlist structure. That means there is nothing to save you if, later, you change the kind keyword for this type from :one to something else. It also means you get no help if you just make a typo when writing the :one symbol. Over the course of developing VL, we found that such issues were very frequent sources of errors!

      Long Form

      In its longer form, natoption/natoptionlist-case allows you to split into cases based on the kind of structure you are looking at. A typical example would be:

      (natoption/natoptionlist-case x
        :one ...
        :list ...)

      It is also possible to consolidate ``uninteresting'' cases using :otherwise.

      For convenience, the case macro automatically binds the fields of x for you, as appropriate for each case. That is, in the :one case, you can use fty::defprod-style foo.bar style accessors for x without having to explicitly add a one b* binder.