• 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
              • Expression-sum-field-list
              • Type
              • Binary-op
                • Binary-op-fix
                • Binary-op-case
                • Binary-opp
                • Binary-op-equiv
                • Binary-op-kind
                • Binary-op-sub
                • Binary-op-rem
                • Binary-op-or
                • Binary-op-ne
                • Binary-op-mul
                • Binary-op-lt
                • Binary-op-le
                • Binary-op-implies
                • Binary-op-implied
                • Binary-op-iff
                • Binary-op-gt
                • Binary-op-ge
                • Binary-op-eq
                • Binary-op-div
                • Binary-op-and
                • Binary-op-add
              • 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
  • Abstract-syntax

Binary-op

Fixtype of Syntheto binary operators.

This is a tagged union type, introduced by fty::deftagsum.

Member Tags → Types
:eq → binary-op-eq
:ne → binary-op-ne
:gt → binary-op-gt
:ge → binary-op-ge
:lt → binary-op-lt
:le → binary-op-le
:and → binary-op-and
:or → binary-op-or
:implies → binary-op-implies
:implied → binary-op-implied
:iff → binary-op-iff
:add → binary-op-add
:sub → binary-op-sub
:mul → binary-op-mul
:div → binary-op-div
:rem → binary-op-rem

There are equality and inequality (for all types), orderings (for integers, characters, and strings), logical boolean connectives (conjunction, disjunction, forward implication, backward implication, coimplication), and arithmetic (for integers), where division rounds towards zero and reminder is defined in the usual way.

Subtopics

Binary-op-fix
Fixing function for binary-op structures.
Binary-op-case
Case macro for the different kinds of binary-op structures.
Binary-opp
Recognizer for binary-op structures.
Binary-op-equiv
Basic equivalence relation for binary-op structures.
Binary-op-kind
Get the kind (tag) of a binary-op structure.
Binary-op-sub
Binary-op-rem
Binary-op-or
Binary-op-ne
Binary-op-mul
Binary-op-lt
Binary-op-le
Binary-op-implies
Binary-op-implied
Binary-op-iff
Binary-op-gt
Binary-op-ge
Binary-op-eq
Binary-op-div
Binary-op-and
Binary-op-add