• 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
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
          • Aij
          • Language
            • Syntax
            • Semantics
              • Primitive-function-macros
              • Primitive-values
                • Floating-pointx-value
                • Doublex-value-fns
                • Primitivex-value
                • Floatx-value-fns
                • Primitive-value
                • Numericx-value
                • Numeric-value
                • Integral-value
                • Int-value
                • Char-value
                • Byte-value
                • Short-value
                • Long-value
                  • Long-valuep
                  • Long-value-fix
                  • Long-value-equiv
                  • Make-long-value
                  • Long-value->int
                    • Change-long-value
                  • Float-value
                  • Double-value
                  • Boolean-value
                  • Floating-point-value
                  • Disjoint-primitive-values
                  • Short-value-list
                  • Long-value-list
                  • Int-value-list
                  • Float-value-list
                  • Double-value-list
                  • Char-value-list
                  • Byte-value-list
                  • Boolean-value-list
                • Floating-point-placeholders
                • Pointers
                • Floating-point-value-set-parameters
                • Values
                • Primitive-operations
                • Primitive-conversions
                • Reference-values
          • 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
    • Long-value

    Long-value->int

    Get the int field from a long-value.

    Signature
    (long-value->int x) → int
    Arguments
    x — Guard (long-valuep x).
    Returns
    int — Type (sbyte64p int).

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

    Definitions and Theorems

    Function: long-value->int$inline

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

    Theorem: sbyte64p-of-long-value->int

    (defthm sbyte64p-of-long-value->int
      (b* ((int (long-value->int$inline x)))
        (sbyte64p int))
      :rule-classes :rewrite)

    Theorem: long-value->int$inline-of-long-value-fix-x

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

    Theorem: long-value->int$inline-long-value-equiv-congruence-on-x

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