		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

Keyword-param-valuep

Does a pretty-printer instruction represent a single object, which could plausibly be the value of a keyword parameter?

Signature
(keyword-param-valuep x eviscp) → bool
Arguments: x — Guard (pinst-p x).; eviscp — Guard (booleanp eviscp).

The only kinds of instructions we don't match are:

KEYPAIR instructions,
FLAT instructions representing dotted objects `. atm',
FLAT instructions representing several objects `a b c', and
KEYWORD instructions, which represent keywords whose associated values are on the next line. These wouldn't be provided as the value of a keyword argument.

Definitions and Theorems

Function: keyword-param-valuep

(defun keyword-param-valuep (x eviscp)
  (declare (xargs :guard (and (pinst-p x) (booleanp eviscp))))
  (let ((acl2::__function__ 'keyword-param-valuep))
    (declare (ignorable acl2::__function__))
    (case (pinst-kind x)
      (:flat (b* ((what (pflat->what (pinst-flat->guts x)))
                  ((when (or (atom what)
                             (and eviscp (evisceratedp what))))
                   nil))
               (not (cdr what))))
      ((:quote :wide :indent) t)
      (otherwise nil))))