• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
            • Grammar
            • Integer-formats
            • Types
            • Portable-ascii-identifiers
            • Values
              • Pointer
              • Member-types-of-member-values
              • Member-value-list->value-list
              • Member-value-list->name-list
              • Expr-value
              • Type-list-of-value-list
              • Type-of-value
              • Value-option
              • Init-value
              • Value-result
              • Type-of-value-option
              • Value-list-result
              • Member-value-list-result
              • Init-value-result
              • Expr-value-result
              • Value-option-result
              • Signed/unsigned-byte-p-of-integer-values
              • Member-type-of-member-value
              • Bounds-of-integer-values
              • Value-promoted-arithmeticp
              • Init-type-of-init-value
              • Value-unsigned-integerp
              • Value-integerp
              • Value-signed-integerp
              • Value-arithmeticp
              • Value-scalarp
              • Value-realp
              • Values/membervalues
                • Value
                • Member-value
                  • Member-value-equiv
                  • Make-member-value
                  • Member-value->value
                    • Member-value->name
                    • Change-member-value
                    • Member-valuep
                    • Member-value-fix
                    • Member-value-count
                  • Value-list
                  • Member-value-list
              • 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
    • Member-value

    Member-value->value

    Get the value field from a member-value.

    Signature
    (member-value->value x) → value
    Arguments
    x — Guard (member-valuep x).
    Returns
    value — Type (valuep value).

    This is an ordinary field accessor created by fty::defprod.

    Definitions and Theorems

    Function: member-value->value$inline

    (defun member-value->value$inline (x)
      (declare (xargs :guard (member-valuep x)))
      (declare (xargs :guard t))
      (let ((__function__ 'member-value->value))
        (declare (ignorable __function__))
        (mbe :logic
             (b* ((x (and t x)))
               (value-fix (cdr (std::da-nth 1 (cdr x)))))
             :exec (cdr (std::da-nth 1 (cdr x))))))

    Theorem: valuep-of-member-value->value

    (defthm valuep-of-member-value->value
      (b* ((value (member-value->value$inline x)))
        (valuep value))
      :rule-classes :rewrite)

    Theorem: member-value->value$inline-of-member-value-fix-x

    (defthm member-value->value$inline-of-member-value-fix-x
      (equal (member-value->value$inline (member-value-fix x))
             (member-value->value$inline x)))

    Theorem: member-value->value$inline-member-value-equiv-congruence-on-x

    (defthm
          member-value->value$inline-member-value-equiv-congruence-on-x
      (implies (member-value-equiv x x-equiv)
               (equal (member-value->value$inline x)
                      (member-value->value$inline x-equiv)))
      :rule-classes :congruence)