• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
          • Language
            • Abstract-syntax
            • Integer-ranges
            • Implementation-environments
            • Dynamic-semantics
            • Static-semantics
              • Check-stmt
              • Check-cond
              • Check-binary-pure
              • Var-table-add-var
              • Check-unary
              • Check-obj-declon
              • Fun-table-add-fun
              • Check-fundef
              • Fun-sinfo
              • Check-expr-asg
              • Check-expr-call
              • Check-arrsub
              • Uaconvert-types
              • Apconvert-type-list
              • Check-initer
              • Adjust-type-list
              • Types+vartab
              • Promote-type
              • Check-tag-declon
              • Check-expr-call-or-asg
              • Check-ext-declon
              • Check-param-declon
              • Check-member
              • Check-expr-pure
              • Init-type-matchp
              • Check-obj-adeclor
              • Check-memberp
              • Check-expr-call-or-pure
              • Check-cast
              • Check-struct-declon-list
              • Check-fun-declor
              • Expr-type
              • Check-ext-declon-list
              • Check-transunit
              • Check-fun-declon
              • Var-defstatus
              • Struct-member-lookup
              • Preprocess
              • Wellformed
              • Check-tyspecseq
              • Check-param-declon-list
              • Check-iconst
              • Check-expr-pure-list
              • Var-sinfo-option
                • Var-sinfo-option-fix
                • Var-sinfo-option-equiv
                • Var-sinfo-option-case
                • Var-sinfo-option-some
                • Var-sinfo-option-none
                • Var-sinfo-optionp
              • Fun-sinfo-option
              • Var-scope-all-definedp
              • Funtab+vartab+tagenv
              • Var-sinfo
              • Var-table-lookup
              • Apconvert-type
              • Var-table
              • Check-tyname
              • Types+vartab-result
              • Funtab+vartab+tagenv-result
              • Fun-table-lookup
              • Wellformed-result
              • Var-table-add-block
              • Var-table-scope
              • Var-table-result
              • Fun-table-result
              • Expr-type-result
              • Adjust-type
              • Check-fileset
              • Var-table-all-definedp
              • Check-const
              • Fun-table-all-definedp
              • Check-ident
              • Fun-table
              • Var-table-init
              • Fun-table-init
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
            • Integer-operations
            • Computation-states
            • Object-designators
            • Operations
            • Errors
            • Tag-environments
            • Function-environments
            • Character-sets
            • Flexible-array-member-removal
            • Arithmetic-operations
            • Pointer-operations
            • Bytes
            • Keywords
            • Real-operations
            • Array-operations
            • Scalar-operations
            • Structure-operations
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Static-semantics

Var-sinfo-option

Fixtype of optional static information about variables.

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

Member Types
:none → var-sinfo-option-none
Represents that no var-sinfo-option is available, i.e., Nothing or None.
:some → var-sinfo-option-some
An available var-sinfo-option, i.e., Just val or Some val.

Subtopics

Var-sinfo-option-fix
Fixing function for var-sinfo-option structures.
Var-sinfo-option-equiv
Basic equivalence relation for var-sinfo-option structures.
Var-sinfo-option-case
Case macro for the different kinds of var-sinfo-option structures.
Var-sinfo-option-some
An available var-sinfo-option, i.e., Just val or Some val.
Var-sinfo-option-none
Represents that no var-sinfo-option is available, i.e., Nothing or None.
Var-sinfo-optionp
Recognizer for var-sinfo-option structures.