Utilities to query `defun-sk` functions.

`defun-sk` mimics functions with (top-level) quantifiers
in the quantifier-free logic of ACL2, by conservatively axiomatizing an associated witness function
and by defining the `defun-sk` function
in terms of the witness function
(either via an actual definition,
or via a definition rule if

These `defun-sk` query utilities provide facilities
to check whether a function has been introduced via `defun-sk`,
and, if so, to retrieve its `defun-sk`-specific constituents.
Constituents of the function that are not `defun-sk`-specific
(formal arguments, guard, etc.)
can be retrieved with more general utilities. Since `defun-sk` extends the `pe-table`
with the `defun-sk` form,
these utilities consult the `pe-table` to determine whether
a function has been introduced by `defun-sk`,
and if that is the case, the `defun-sk`-specific components
are retrieved based on the expected structure of
the `defun-sk` form and of the forms it generates
(`encapsulate`, `defchoose`, etc.).
Thus, if the `pe-table` is extended
with a form starting with `defun-sk`
without using `defun-sk`
(by directly calling `extend-pe-table`),
these utilities, as currently implemented,
can be fooled and return meaningless results.
(These utilities could be extended to defensively check
that the form and its expansion have the right structure,
if that becomes important.)

- Defun-sk-matrix
- Retrieve the matrix of a function introduced via
`defun-sk`, in untranslated form. - Defun-sk-p
- Check if a named function has been introduced via
`defun-sk`, returning the function's`defun-sk`form if the check succeeds. - Defun-sk-namep
- Recognize symbols
that name functions introduced via
`defun-sk`. - Defun-sk-body
- Retrieve the body of a function introduced via
`defun-sk`. - Defun-sk-imatrix
- Retrieve the matrix of a function introduced via
`defun-sk`, in untranslated form. - Defun-sk-definition-name
- Retrieve the name of the definition rule of
a function introduced via
`defun-sk`. - Defun-sk-witness
- Retrieve the name of the witness of
a function introduced via
`defun-sk`. - Defun-sk-classicalp
- Retrieve the value of the
:classicalp option of a function introduced via`defun-sk`. - Defun-sk-rewrite-kind
- Retrieve the kind of the rewrite rule of
a function introduced via
`defun-sk`. - Defun-sk-rewrite-name
- Retrieve the name of the rewrite rule of
a function introduced via
`defun-sk`. - Defun-sk-rewrite-kind-p
- Kinds of rewrite rules associated to
`defun-sk`functions with the universal quantifier. - Defun-sk-quantifier
- Retrieve the quantifier of
a function introduced via
`defun-sk`. - Defun-sk-options
- Retrieve the keyed options of
a function introduced via
`defun-sk`. - Defun-sk-bound-vars
- Retrieve the bound variables of
a function introduced via
`defun-sk`. - Defun-sk-strengthen
- Retrieve the value of the
:strengthen option of a function introduced via`defun-sk`. - Defun-sk-quantifier-p
- Existential and universal quantifiers.