		Search-engine friendly clone of the ACL2 documentation.

Expressions

Vl-arity-fix

Signature
(vl-arity-fix op args) → *
Arguments: op — Guard (vl-op-p op).

Definitions and Theorems

Function: vl-arity-fix$inline

(defun vl-arity-fix$inline (op args)
  (declare (xargs :guard (vl-op-p op)))
  (declare (xargs :guard (vl-arity-ok-p op args)))
  (let ((__function__ 'vl-arity-fix))
    (declare (ignorable __function__))
    (mbe :logic
         (let ((arity (vl-op-arity op))
               (len (len args)))
           (cond ((or (not arity) (equal len arity))
                  args)
                 ((< arity len) (take arity args))
                 (t (append args
                            (replicate (- arity len)
                                       *vl-default-expr*)))))
         :exec args)))

Theorem: vl-arity-ok-p-of-vl-arity-fix

(defthm vl-arity-ok-p-of-vl-arity-fix
  (vl-arity-ok-p op (vl-arity-fix op args)))

Theorem: vl-arity-fix-when-vl-arity-ok-p

(defthm vl-arity-fix-when-vl-arity-ok-p
  (implies (vl-arity-ok-p op args)
           (equal (vl-arity-fix op args) args)))

Theorem: vl-arity-fix$inline-of-vl-op-fix-op

(defthm vl-arity-fix$inline-of-vl-op-fix-op
  (equal (vl-arity-fix$inline (vl-op-fix op)
                              args)
         (vl-arity-fix$inline op args)))

Theorem: vl-arity-fix$inline-vl-op-equiv-congruence-on-op

(defthm vl-arity-fix$inline-vl-op-equiv-congruence-on-op
  (implies (vl-op-equiv op op-equiv)
           (equal (vl-arity-fix$inline op args)
                  (vl-arity-fix$inline op-equiv args)))
  :rule-classes :congruence)