• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Error-checking
        • Apt
        • Abnf
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Prime-field-constraint-systems
        • Soft
        • Bv
        • Imp-language
        • Event-macros
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
          • Primitive-functions
          • Translated-terms
          • Values
            • Value
              • Valuep
              • Value-case
              • Value-fix
              • Value-equiv
              • Value-count
              • Value-cons
              • Value-symbol
              • Value-string
              • Value-number
                • Value-number->get
                  • Make-value-number
                  • Change-value-number
                • Value-character
                • Value-kind
              • Symbol-value
              • Lower-symbol
              • Lift-symbol-list
              • Symbol-value-option
              • Value-option
              • Lift-value
              • Lift-symbol
              • Value-rational->get
              • Value-integer->get
              • Value-case-rational
              • Value-case-integer
              • Value-symbol-list
              • Value-list-of
              • Lower-value
              • Value-list
              • Symbol-value-list
              • Symbol-value-set
              • Value-nil
              • Value-t
            • Evaluation
            • Program-equivalence
            • Functions
            • Packages
            • Programs
            • Interpreter
            • Evaluation-states
          • Prime-fields
          • Java
          • C
          • Syntheto
          • Number-theory
          • Cryptography
          • Lists-light
          • File-io-light
          • Json
          • Built-ins
          • Solidity
          • Axe
          • Std-extensions
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Execloader
        • Axe
      • Testing-utilities
      • Math
    • Value-number

    Value-number->get

    Get the get field from a value-number.

    Signature
    (value-number->get x) → get
    Arguments
    x — Guard (valuep x).
    Returns
    get — Type (acl2-numberp get).

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

    Definitions and Theorems

    Function: value-number->get$inline

    (defun
       value-number->get$inline (x)
       (declare (xargs :guard (valuep x)))
       (declare (xargs :guard (equal (value-kind x) :number)))
       (let ((__function__ 'value-number->get))
            (declare (ignorable __function__))
            (mbe :logic (b* ((x (and (equal (value-kind x) :number) x)))
                            (fix (std::da-nth 0 (cdr x))))
                 :exec (std::da-nth 0 (cdr x)))))

    Theorem: acl2-numberp-of-value-number->get

    (defthm acl2-numberp-of-value-number->get
            (b* ((get (value-number->get$inline x)))
                (acl2-numberp get))
            :rule-classes :rewrite)

    Theorem: value-number->get$inline-of-value-fix-x

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

    Theorem: value-number->get$inline-value-equiv-congruence-on-x

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

    Theorem: value-number->get-when-wrong-kind

    (defthm value-number->get-when-wrong-kind
            (implies (not (equal (value-kind x) :number))
                     (equal (value-number->get x)
                            (fix nil))))