		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-namep

Recognize symbols that name functions introduced via defun-sk.

Signature
(defun-sk-namep x wrld) → yes/no
Arguments: wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

This function is enabled because it is meant as an abbreviation. Thus, theorems triggered by this function should be avoided.

Definitions and Theorems

Function: defun-sk-namep

(defun defun-sk-namep (x wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'defun-sk-namep))
    (declare (ignorable __function__))
    (and (function-namep x wrld)
         (defun-sk-p x wrld)
         t)))

Theorem: booleanp-of-defun-sk-namep

(defthm booleanp-of-defun-sk-namep
  (b* ((yes/no (defun-sk-namep x wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)