• 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
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
          • Process-syntheto-toplevel-fn
          • Translation
          • Language
            • Static-semantics
            • Abstract-syntax
              • Expression
                • Expressionp
                • Expression-case
                • Expression-sum-field
                • Expression-sum-update
                • Expression-equiv
                • Expression-kind
                • Expression-product-field
                • Expression-when
                • Expression-unless
                • Expression-sum-test
                • Expression-sum-construct
                • Expression-product-update
                • Expression-if
                • Expression-call
                • Expression-bind
                • Expression-binary
                  • Expression-binary->right-operand
                  • Make-expression-binary
                  • Expression-binary->left-operand
                  • Expression-binary->operator
                  • Change-expression-binary
                • Expression-product-construct
                • Expression-unary
                • Expression-component
                • Expression-variable
                • Expression-multi
                • Expression-literal
                • Expression-cond
                • Expression-bad-expression
                • Expression-fix
                • Expression-count
              • Expression-sum-field-list
              • Type
              • Binary-op
              • Expression-product-field-list
              • Abstract-syntax-operations
              • Function-definition-list->header-list
              • Type-definition-list->name-list
              • Initializer-list->value-list
              • Function-header-list->name-list
              • Typed-variable-list->type-list
              • Typed-variable-list->name-list
              • Branch-list->condition-list
              • Alternative-list->name-list
              • Function-specifier
              • Expression-variable-list
              • Type-subset
              • Field-list->type-list
              • Field-list->name-list
              • Function-specification
              • Identifier
              • Toplevel
              • Function-definer
              • Function-header
              • Type-definer
              • Literal
              • Type-product
              • Function-definition
              • Type-sum
              • Maybe-expression
              • Transform-argument-value
              • Transform
              • Theorem
              • Quantifier
              • Maybe-function-specification
              • Maybe-typed-variable
              • Maybe-type-definition
              • Maybe-function-header
              • Maybe-function-definition
              • Maybe-type-sum
              • Maybe-type-subset
              • Maybe-type-product
              • Maybe-type-definer
              • Maybe-theorem
              • Maybe-type
              • Initializer
              • Type-definition
              • Alternative
              • Unary-op
              • Typed-variable
              • Branch
              • Field
              • Transform-argument
              • Type-recursion
              • Program
              • Function-recursion
              • Typed-variable-list
              • Toplevel-name
              • Toplevel-list
              • Initializer-list
              • Expression-fixtypes
              • Toplevel-fn-names
              • Lookup-transform-argument
              • Function-definition-names
              • Type-definition-list
              • Transform-argument-list
              • Function-header-list
              • Function-definition-list
              • Alternative-list
              • Type-list
              • Identifier-set
              • Identifier-list
              • Field-list
              • Expression-list
              • Branch-list
              • Extract-default-param-alist
              • Create-arg-defaults-table
            • Outcome
            • Abstract-syntax-operations
            • Outcome-list
            • Outcomes
          • Process-syntheto-toplevel
          • Shallow-embedding
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Expression

Expression-binary

This is a product type, introduced by fty::deftagsum in support of expression.

Fields
operator — binary-op
left-operand — expression
right-operand — expression

Subtopics

Expression-binary->right-operand
Get the right-operand field from a expression-binary.
Make-expression-binary
Basic constructor macro for expression-binary structures.
Expression-binary->left-operand
Get the left-operand field from a expression-binary.
Expression-binary->operator
Get the operator field from a expression-binary.
Change-expression-binary
Modifying constructor for expression-binary structures.