• 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
              • Tyspecseq
              • Expr
                • Exprp
                • Expr-case
                • Expr-binary
                  • Make-expr-binary
                  • Expr-binary->op
                  • Expr-binary->arg2
                  • Expr-binary->arg1
                    • Change-expr-binary
                  • Expr-equiv
                  • Expr-cond
                  • Expr-unary
                  • Expr-memberp
                  • Expr-member
                  • Expr-cast
                  • Expr-call
                  • Expr-arrsub
                  • Expr-kind
                  • Expr-preinc
                  • Expr-predec
                  • Expr-postinc
                  • Expr-postdec
                  • Expr-ident
                  • Expr-const
                  • Expr-fix
                  • Expr-count
                • Binop
                • Fileset
                • Obj-declor
                • Ident
                • Iconst
                • Obj-adeclor
                • Abstract-syntax-operations
                • Const
                • Fundef
                • Unop
                • File
                • Tag-declon
                • Fun-declor
                • Obj-declon
                • Iconst-length
                • Label
                • Struct-declon
                • Initer
                • Ext-declon
                • Fun-adeclor
                • Expr-option
                • Iconst-base
                • Initer-option
                • Iconst-option
                • Tyspecseq-option
                • Stmt-option
                • Scspecseq
                • Param-declon
                • Obj-declon-option
                • File-option
                • Tyname
                • Transunit
                • Fun-declon
                • Transunit-result
                • Param-declon-list
                • Struct-declon-list
                • Expr-list
                • Tyspecseq-list
                • Ident-set
                • Ident-list
                • Ext-declon-list
                • Unop-list
                • Tyname-list
                • Fundef-list
                • Fun-declon-list
                • Binop-list
                • Stmt-fixtypes
                • Expr-fixtypes
              • Integer-ranges
              • Implementation-environments
              • Dynamic-semantics
              • Static-semantics
              • 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
    • Expr-binary

    Expr-binary->arg1

    Get the arg1 field from a expr-binary.

    Signature
    (expr-binary->arg1 x) → arg1
    Arguments
    x — Guard (exprp x).
    Returns
    arg1 — Type (exprp arg1).

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

    Definitions and Theorems

    Function: expr-binary->arg1$inline

    (defun expr-binary->arg1$inline (x)
      (declare (xargs :guard (exprp x)))
      (declare (xargs :guard (equal (expr-kind x) :binary)))
      (let ((__function__ 'expr-binary->arg1))
        (declare (ignorable __function__))
        (mbe :logic
             (b* ((x (and (equal (expr-kind x) :binary) x)))
               (expr-fix (std::da-nth 1 (cdr x))))
             :exec (std::da-nth 1 (cdr x)))))

    Theorem: exprp-of-expr-binary->arg1

    (defthm exprp-of-expr-binary->arg1
      (b* ((arg1 (expr-binary->arg1$inline x)))
        (exprp arg1))
      :rule-classes :rewrite)

    Theorem: expr-binary->arg1$inline-of-expr-fix-x

    (defthm expr-binary->arg1$inline-of-expr-fix-x
      (equal (expr-binary->arg1$inline (expr-fix x))
             (expr-binary->arg1$inline x)))

    Theorem: expr-binary->arg1$inline-expr-equiv-congruence-on-x

    (defthm expr-binary->arg1$inline-expr-equiv-congruence-on-x
      (implies (expr-equiv x x-equiv)
               (equal (expr-binary->arg1$inline x)
                      (expr-binary->arg1$inline x-equiv)))
      :rule-classes :congruence)

    Theorem: expr-binary->arg1-when-wrong-kind

    (defthm expr-binary->arg1-when-wrong-kind
      (implies (not (equal (expr-kind x) :binary))
               (equal (expr-binary->arg1 x)
                      (expr-fix nil))))