• 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
        • Primitive-functions
          • Eval-intern-in-package-of-symbol
          • Eval-pkg-witness
          • Eval-pkg-imports
          • Primitive-function-namep
          • Primitive-function-arity
          • Eval-if
          • Eval-bad-atom<=
          • Eval-<
          • Eval-coerce
          • Eval-complex
          • Eval-binary-+
          • Eval-binary-*
          • Eval-equal
          • Eval-cons
          • Eval-symbol-package-name
          • Eval-complex-rationalp
          • Eval-unary-/
          • Eval-symbol-name
          • Eval-denominator
          • Eval-code-char
          • Eval-unary--
          • Eval-realpart
          • Eval-rationalp
          • Eval-numerator
          • Eval-integerp
          • Eval-imagpart
          • Eval-characterp
          • Eval-char-code
          • Eval-ACL2-numberp
          • Eval-symbolp
          • Eval-stringp
          • Eval-consp
          • Eval-cdr
          • Eval-car
        • Translated-terms
        • Values
        • Evaluation
        • Program-equivalence
        • Functions
        • Packages
        • Programs
        • Interpreter
        • Evaluation-states
      • 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

• Primitive-functions

Primitive-function-namep

Check if a symbol value is the name of a primitive function.

Signature

(primitive-function-namep name) → yes/no

Arguments

name — Guard (symbol-valuep name).

Returns

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

Definitions and Theorems

Function: primitive-function-namep

(defun primitive-function-namep (name)
 (declare (xargs :guard (symbol-valuep name)))
 (let ((__function__ 'primitive-function-namep))
  (declare (ignorable __function__))
  (or
     (symbol-value-equiv name (lift-symbol 'acl2-numberp))
     (symbol-value-equiv name (lift-symbol 'rationalp))
     (symbol-value-equiv name (lift-symbol 'integerp))
     (symbol-value-equiv name (lift-symbol 'complex-rationalp))
     (symbol-value-equiv name (lift-symbol 'complex))
     (symbol-value-equiv name (lift-symbol 'realpart))
     (symbol-value-equiv name (lift-symbol 'imagpart))
     (symbol-value-equiv name (lift-symbol 'numerator))
     (symbol-value-equiv name (lift-symbol 'denominator))
     (symbol-value-equiv name (lift-symbol 'unary--))
     (symbol-value-equiv name (lift-symbol 'unary-/))
     (symbol-value-equiv name (lift-symbol 'binary-+))
     (symbol-value-equiv name (lift-symbol 'binary-*))
     (symbol-value-equiv name (lift-symbol '<))
     (symbol-value-equiv name (lift-symbol 'characterp))
     (symbol-value-equiv name (lift-symbol 'char-code))
     (symbol-value-equiv name (lift-symbol 'code-char))
     (symbol-value-equiv name (lift-symbol 'stringp))
     (symbol-value-equiv name (lift-symbol 'coerce))
     (symbol-value-equiv name (lift-symbol 'symbolp))
     (symbol-value-equiv name (lift-symbol 'symbol-package-name))
     (symbol-value-equiv name (lift-symbol 'symbol-name))
     (symbol-value-equiv name
                         (lift-symbol 'intern-in-package-of-symbol))
     (symbol-value-equiv name (lift-symbol 'consp))
     (symbol-value-equiv name (lift-symbol 'cons))
     (symbol-value-equiv name (lift-symbol 'car))
     (symbol-value-equiv name (lift-symbol 'cdr))
     (symbol-value-equiv name (lift-symbol 'pkg-imports))
     (symbol-value-equiv name (lift-symbol 'pkg-witness))
     (symbol-value-equiv name (lift-symbol 'equal))
     (symbol-value-equiv name (lift-symbol 'if))
     (symbol-value-equiv name (lift-symbol 'acl2::bad-atom<=)))))

Theorem: booleanp-of-primitive-function-namep

(defthm booleanp-of-primitive-function-namep
  (b* ((yes/no (primitive-function-namep name)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: primitive-function-namep-of-symbol-value-fix-name

(defthm primitive-function-namep-of-symbol-value-fix-name
  (equal (primitive-function-namep (symbol-value-fix name))
         (primitive-function-namep name)))

Theorem: primitive-function-namep-symbol-value-equiv-congruence-on-name

(defthm
     primitive-function-namep-symbol-value-equiv-congruence-on-name
  (implies (symbol-value-equiv name name-equiv)
           (equal (primitive-function-namep name)
                  (primitive-function-namep name-equiv)))
  :rule-classes :congruence)