		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-paramdecl-set-default

Signature
(vl-paramdecl-set-default x val) → (mv ok new-x)
Arguments: x — Guard (vl-paramdecl-p x).; val — Guard (vl-maybe-paramvalue-p val).
Returns: new-x — Type (vl-paramdecl-p new-x).

Definitions and Theorems

Function: vl-paramdecl-set-default

(defun vl-paramdecl-set-default (x val)
 (declare (xargs :guard (and (vl-paramdecl-p x)
                             (vl-maybe-paramvalue-p val))))
 (let ((__function__ 'vl-paramdecl-set-default))
  (declare (ignorable __function__))
  (b*
   (((vl-paramdecl x))
    (val (vl-maybe-paramvalue-fix val))
    ((mv ok type)
     (vl-paramtype-case
       x.type :vl-typeparam
       (if
        (or (not val)
            (vl-paramvalue-case val :type))
        (mv t
            (change-vl-typeparam
                 x.type
                 :default (and val (vl-paramvalue-type->type val))))
        (mv nil
            (change-vl-typeparam x.type
                                 :default nil)))
       :vl-implicitvalueparam
       (if
        (or (not val)
            (vl-paramvalue-case val :expr))
        (mv t
            (change-vl-implicitvalueparam
                 x.type
                 :default (and val (vl-paramvalue-expr->expr val))))
        (mv nil
            (change-vl-implicitvalueparam x.type
                                          :default nil)))
       :vl-explicitvalueparam
       (if
        (or (not val)
            (vl-paramvalue-case val :expr))
        (mv t
            (change-vl-explicitvalueparam
                 x.type
                 :default (and val (vl-paramvalue-expr->expr val))))
        (mv nil
            (change-vl-explicitvalueparam x.type
                                          :default nil))))))
   (mv ok
       (change-vl-paramdecl x :type type)))))

Theorem: vl-paramdecl-p-of-vl-paramdecl-set-default.new-x

(defthm vl-paramdecl-p-of-vl-paramdecl-set-default.new-x
  (b* (((mv ?ok ?new-x)
        (vl-paramdecl-set-default x val)))
    (vl-paramdecl-p new-x))
  :rule-classes :rewrite)

Theorem: vl-paramdecl-set-default-of-vl-paramdecl-fix-x

(defthm vl-paramdecl-set-default-of-vl-paramdecl-fix-x
  (equal (vl-paramdecl-set-default (vl-paramdecl-fix x)
                                   val)
         (vl-paramdecl-set-default x val)))

Theorem: vl-paramdecl-set-default-vl-paramdecl-equiv-congruence-on-x

(defthm vl-paramdecl-set-default-vl-paramdecl-equiv-congruence-on-x
  (implies (vl-paramdecl-equiv x x-equiv)
           (equal (vl-paramdecl-set-default x val)
                  (vl-paramdecl-set-default x-equiv val)))
  :rule-classes :congruence)

Theorem: vl-paramdecl-set-default-of-vl-maybe-paramvalue-fix-val

(defthm vl-paramdecl-set-default-of-vl-maybe-paramvalue-fix-val
  (equal (vl-paramdecl-set-default x (vl-maybe-paramvalue-fix val))
         (vl-paramdecl-set-default x val)))

Theorem: vl-paramdecl-set-default-vl-maybe-paramvalue-equiv-congruence-on-val

(defthm
 vl-paramdecl-set-default-vl-maybe-paramvalue-equiv-congruence-on-val
 (implies (vl-maybe-paramvalue-equiv val val-equiv)
          (equal (vl-paramdecl-set-default x val)
                 (vl-paramdecl-set-default x val-equiv)))
 :rule-classes :congruence)