		Search-engine friendly clone of the ACL2 documentation.

Defchoose-queries

Defchoosep

Check if a function was introduced via defchoose, returning the function's constraining axiom if the check succeeds.

Signature
(defchoosep fn wrld) → axiom
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: axiom — A pseudo-termp.

If the check fails, nil is returned.

A function introduced via defchoose is recognizable by the presence of the defchoose-axiom property, which is the axiom that constrains the function.

This utility causes an error if called on a symbol that is not a function symbol.

Definitions and Theorems

Function: defchoosep

(defun defchoosep (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'defchoosep))
    (declare (ignorable __function__))
    (if (not (function-symbolp fn wrld))
        (raise "The symbol ~x0 does not name a function."
               fn)
      (getpropc fn 'defchoose-axiom
                nil wrld))))