		Search-engine friendly clone of the ACL2 documentation.

Svex

Svcall*

Safely construct an svex for a function call, with evaluation of quotes and simplification of concatenations and right-shifts.

Definitions and Theorems

Function: svcall*-fn

(defun svcall*-fn (fn args)
  (declare (xargs :guard t))
  (b* ((look (assoc fn *svex-op-table*))
       ((unless look)
        (er hard? 'svcall*
            "Svex function doesn't exist: ~x0" fn))
       (formals (third look))
       ((unless (eql (len formals) (len args)))
        (er hard? 'svcall*
            "Wrong arity for call of ~x0" fn)))
    (cons 'svex-call*
          (cons (cons 'quote (cons fn 'nil))
                (cons (cons 'list args) 'nil)))))