		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-definition-name

Retrieve the name of the definition rule of a function introduced via defun-sk.

Signature
(defun-sk-definition-name fn wrld) → name
Arguments: fn — Guard (defun-sk-namep fn wrld).; wrld — Guard (plist-worldp wrld).
Returns: name — A symbolp.

This is relevant when :constrain is not nil: the result is the name of the theorem that essentially defines fn, but leaving fn technically just constrained, not defined. Otherwise, nil is returned.

Definitions and Theorems

Function: defun-sk-definition-name

(defun defun-sk-definition-name (fn wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (defun-sk-namep fn wrld))))
  (let ((__function__ 'defun-sk-definition-name))
    (declare (ignorable __function__))
    (b* ((options (defun-sk-options fn wrld))
         (pair (assoc-eq :constrain options))
         ((when (null pair)) nil)
         (option (cdr pair)))
      (if (eq option t)
          (add-suffix fn "-DEFINITION")
        option))))