		Search-engine friendly clone of the ACL2 documentation.

Edgesplit

Vl-edgesplit-stmt-for-lvalue

Determine a splittable statement's effect on a single lvalue.

Signature
(vl-edgesplit-stmt-for-lvalue x lvalue) → stmt
Arguments: x — Statement we're splitting into multiple always blocks.
Guard (and (vl-stmt-p x) (vl-edgesplitstmt-p x)).; lvalue — Particular lvalue we're splitting it up for.
Guard (stringp lvalue).
Returns: stmt — Type (vl-stmt-p stmt), given the guard.

Theorem: return-type-of-vl-edgesplit-stmt-for-lvalue.stmt

(defthm return-type-of-vl-edgesplit-stmt-for-lvalue.stmt
  (implies (and (force (if (vl-stmt-p x)
                           (vl-edgesplitstmt-p x)
                         'nil))
                (force (stringp lvalue)))
           (b* ((?stmt (vl-edgesplit-stmt-for-lvalue x lvalue)))
             (vl-stmt-p stmt)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-edgesplit-stmtlist-for-lvalue.stmts

(defthm return-type-of-vl-edgesplit-stmtlist-for-lvalue.stmts
 (implies (and (force (if (vl-stmtlist-p x)
                          (vl-edgesplitstmtlist-p x)
                        'nil))
               (force (stringp lvalue)))
          (b* ((?stmts (vl-edgesplit-stmtlist-for-lvalue x lvalue)))
            (vl-stmtlist-p stmts)))
 :rule-classes :rewrite)

Subtopics

Vl-edgesplit-stmtlist-for-lvalue