		Search-engine friendly clone of the ACL2 documentation.

Defmapping-table

Defmapping-filter-call

Remove any :print and :show-only inputs from a call of defmapping or its wrappers.

Signature
(defmapping-filter-call call) → call$
Arguments: call — Guard (pseudo-event-formp call).
Returns: call$ — A pseudo-event-formp.

As explained in the documentation, these two options are ignored when checking redundancy.

Definitions and Theorems

Function: defmapping-filter-call

(defun defmapping-filter-call (call)
 (declare (xargs :guard (pseudo-event-formp call)))
 (declare
  (xargs
      :guard (and (>= (len call) 6)
                  (member-eq (car call)
                             '(defmapping defiso defsurj definj)))))
 (let ((__function__ 'defmapping-filter-call))
  (declare (ignorable __function__))
  (b*
   ((number-of-required-args 5)
    (number-of-elements-before-options (1+ number-of-required-args))
    (options (nthcdr number-of-elements-before-options call))
    (options (remove-keyword :print options))
    (options (remove-keyword :show-only options))
    (call$ (append (take number-of-elements-before-options call)
                   options)))
   call$)))