• 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
          • Outcome
          • Abstract-syntax-operations
            • Subst-expression-fns
            • Field-list-to-typed-variable-list
            • Negate-expression
            • Get-function-definition-in-function-definitions
            • Get-function-definition
            • Get-type-definition-in-type-definitions
            • Get-type-definition
            • Get-function-specification
            • Get-type-subset
            • Get-alternative-product
            • Direct-supertype
            • Get-function-header-in-list
            • Equate-expression-lists
            • Get-field-type
            • Get-theorem
            • Get-defined-type-names-in-type-definitions
            • Disjoin-expressions
            • Conjoin-expressions
            • Get-type-product
            • Binary-op-nonstrictp
            • Get-type-sum
            • Get-defined-type-names
            • Equate-expressions
            • Field-to-typed-variable
            • Subst-expression
            • Binary-op-strictp
            • Initializer-list-from-flds-vals
            • Typed-variable-list->-expression-variable-list
            • Typed-variable-list->-expression
            • Variable-substitution
            • Local-variables
            • Identifier-list-names
            • Functions-called
            • Subst-expression-list
            • Subst-branch-list
            • Subst-branch
          • 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-operations

Binary-op-nonstrictp

Check if a binary operator is non-strict.

Signature

(binary-op-nonstrictp op) → yes/no

Arguments

op — Guard (binary-opp op).

Returns

yes/no — Type (booleanp yes/no).

In Syntheto, some boolean connectives are non-strict, in the sense that one operand can assume the truth or falsehood of the other operand to discharge its type obligations. This is because the value of the result may be determined just by one operand value in some cases. See the static semantics for details.

Definitions and Theorems

Function: binary-op-nonstrictp

(defun binary-op-nonstrictp (op)
  (declare (xargs :guard (binary-opp op)))
  (let ((__function__ 'binary-op-nonstrictp))
    (declare (ignorable __function__))
    (and (member-eq (binary-op-kind op)
                    '(:and :or :implies :implied))
         t)))

Theorem: booleanp-of-binary-op-nonstrictp

(defthm booleanp-of-binary-op-nonstrictp
  (b* ((yes/no (binary-op-nonstrictp op)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: binary-op-nonstrictp-of-binary-op-fix-op

(defthm binary-op-nonstrictp-of-binary-op-fix-op
  (equal (binary-op-nonstrictp (binary-op-fix op))
         (binary-op-nonstrictp op)))

Theorem: binary-op-nonstrictp-binary-op-equiv-congruence-on-op

(defthm binary-op-nonstrictp-binary-op-equiv-congruence-on-op
  (implies (binary-op-equiv op op-equiv)
           (equal (binary-op-nonstrictp op)
                  (binary-op-nonstrictp op-equiv)))
  :rule-classes :congruence)