		Search-engine friendly clone of the ACL2 documentation.

Verilog-printing

Vl-pp-expr

Main pretty-printer for an expression.

Signature
(vl-pp-expr x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-expr-p x).

Theorem: vl-pp-indexlist-fn-of-vl-exprlist-fix-x

(defthm vl-pp-indexlist-fn-of-vl-exprlist-fix-x
  (equal (vl-pp-indexlist-fn (vl-exprlist-fix x)
                             ps)
         (vl-pp-indexlist-fn x ps)))

Theorem: vl-pp-hidindex-fn-of-vl-hidindex-fix-x

(defthm vl-pp-hidindex-fn-of-vl-hidindex-fix-x
  (equal (vl-pp-hidindex-fn (vl-hidindex-fix x)
                            ps)
         (vl-pp-hidindex-fn x ps)))

Theorem: vl-pp-hidexpr-fn-of-vl-hidexpr-fix-x

(defthm vl-pp-hidexpr-fn-of-vl-hidexpr-fix-x
  (equal (vl-pp-hidexpr-fn (vl-hidexpr-fix x) ps)
         (vl-pp-hidexpr-fn x ps)))

Theorem: vl-pp-scopeexpr-fn-of-vl-scopeexpr-fix-x

(defthm vl-pp-scopeexpr-fn-of-vl-scopeexpr-fix-x
  (equal (vl-pp-scopeexpr-fn (vl-scopeexpr-fix x)
                             ps)
         (vl-pp-scopeexpr-fn x ps)))

Theorem: vl-pp-range-fn-of-vl-range-fix-x

(defthm vl-pp-range-fn-of-vl-range-fix-x
  (equal (vl-pp-range-fn (vl-range-fix x) ps)
         (vl-pp-range-fn x ps)))

Theorem: vl-pp-plusminus-fn-of-vl-plusminus-fix-x

(defthm vl-pp-plusminus-fn-of-vl-plusminus-fix-x
  (equal (vl-pp-plusminus-fn (vl-plusminus-fix x)
                             ps)
         (vl-pp-plusminus-fn x ps)))

Theorem: vl-pp-partselect-fn-of-vl-partselect-fix-x

(defthm vl-pp-partselect-fn-of-vl-partselect-fix-x
  (equal (vl-pp-partselect-fn (vl-partselect-fix x)
                              ps)
         (vl-pp-partselect-fn x ps)))

Theorem: vl-pp-arrayrange-fn-of-vl-arrayrange-fix-x

(defthm vl-pp-arrayrange-fn-of-vl-arrayrange-fix-x
  (equal (vl-pp-arrayrange-fn (vl-arrayrange-fix x)
                              ps)
         (vl-pp-arrayrange-fn x ps)))

Theorem: vl-pp-streamexpr-fn-of-vl-streamexpr-fix-x

(defthm vl-pp-streamexpr-fn-of-vl-streamexpr-fix-x
  (equal (vl-pp-streamexpr-fn (vl-streamexpr-fix x)
                              ps)
         (vl-pp-streamexpr-fn x ps)))

Theorem: vl-pp-streamexprlist-fn-of-vl-streamexprlist-fix-x

(defthm vl-pp-streamexprlist-fn-of-vl-streamexprlist-fix-x
  (equal (vl-pp-streamexprlist-fn (vl-streamexprlist-fix x)
                                  ps)
         (vl-pp-streamexprlist-fn x ps)))

Theorem: vl-pp-valuerange-fn-of-vl-valuerange-fix-x

(defthm vl-pp-valuerange-fn-of-vl-valuerange-fix-x
  (equal (vl-pp-valuerange-fn (vl-valuerange-fix x)
                              ps)
         (vl-pp-valuerange-fn x ps)))

Theorem: vl-pp-valuerangelist-fn-of-vl-valuerangelist-fix-x

(defthm vl-pp-valuerangelist-fn-of-vl-valuerangelist-fix-x
  (equal (vl-pp-valuerangelist-fn (vl-valuerangelist-fix x)
                                  ps)
         (vl-pp-valuerangelist-fn x ps)))

Theorem: vl-pp-patternkey-fn-of-vl-patternkey-fix-x

(defthm vl-pp-patternkey-fn-of-vl-patternkey-fix-x
  (equal (vl-pp-patternkey-fn (vl-patternkey-fix x)
                              ps)
         (vl-pp-patternkey-fn x ps)))

Theorem: vl-pp-keyvallist-fn-of-vl-keyvallist-fix-x

(defthm vl-pp-keyvallist-fn-of-vl-keyvallist-fix-x
  (equal (vl-pp-keyvallist-fn (vl-keyvallist-fix x)
                              ps)
         (vl-pp-keyvallist-fn x ps)))

Theorem: vl-pp-assignpat-fn-of-vl-assignpat-fix-x

(defthm vl-pp-assignpat-fn-of-vl-assignpat-fix-x
  (equal (vl-pp-assignpat-fn (vl-assignpat-fix x)
                             ps)
         (vl-pp-assignpat-fn x ps)))

Theorem: vl-pp-casttype-fn-of-vl-casttype-fix-x

(defthm vl-pp-casttype-fn-of-vl-casttype-fix-x
  (equal (vl-pp-casttype-fn (vl-casttype-fix x)
                            ps)
         (vl-pp-casttype-fn x ps)))

Theorem: vl-pp-expr-fn-of-vl-expr-fix-x

(defthm vl-pp-expr-fn-of-vl-expr-fix-x
  (equal (vl-pp-expr-fn (vl-expr-fix x) ps)
         (vl-pp-expr-fn x ps)))

Theorem: vl-pp-exprlist-fn-of-vl-exprlist-fix-x

(defthm vl-pp-exprlist-fn-of-vl-exprlist-fix-x
  (equal (vl-pp-exprlist-fn (vl-exprlist-fix x)
                            ps)
         (vl-pp-exprlist-fn x ps)))

Theorem: vl-pp-maybe-exprlist-fn-of-vl-maybe-exprlist-fix-x

(defthm vl-pp-maybe-exprlist-fn-of-vl-maybe-exprlist-fix-x
  (equal (vl-pp-maybe-exprlist-fn (vl-maybe-exprlist-fix x)
                                  ps)
         (vl-pp-maybe-exprlist-fn x ps)))

Theorem: vl-pp-call-namedargs-fn-of-vl-call-namedargs-fix-x

(defthm vl-pp-call-namedargs-fn-of-vl-call-namedargs-fix-x
  (equal (vl-pp-call-namedargs-fn (vl-call-namedargs-fix x)
                                  ps)
         (vl-pp-call-namedargs-fn x ps)))

Theorem: vl-pp-atts-aux-fn-of-vl-atts-fix-x

(defthm vl-pp-atts-aux-fn-of-vl-atts-fix-x
  (equal (vl-pp-atts-aux-fn (vl-atts-fix x) ps)
         (vl-pp-atts-aux-fn x ps)))

Theorem: vl-pp-atts-fn-of-vl-atts-fix-x

(defthm vl-pp-atts-fn-of-vl-atts-fix-x
  (equal (vl-pp-atts-fn (vl-atts-fix x) ps)
         (vl-pp-atts-fn x ps)))

Theorem: vl-pp-datatype-fn-of-vl-datatype-fix-x

(defthm vl-pp-datatype-fn-of-vl-datatype-fix-x
  (equal (vl-pp-datatype-fn (vl-datatype-fix x)
                            ps)
         (vl-pp-datatype-fn x ps)))

Theorem: vl-pp-structmemberlist-fn-of-vl-structmemberlist-fix-x

(defthm vl-pp-structmemberlist-fn-of-vl-structmemberlist-fix-x
  (equal (vl-pp-structmemberlist-fn (vl-structmemberlist-fix x)
                                    ps)
         (vl-pp-structmemberlist-fn x ps)))

Theorem: vl-pp-structmember-fn-of-vl-structmember-fix-x

(defthm vl-pp-structmember-fn-of-vl-structmember-fix-x
  (equal (vl-pp-structmember-fn (vl-structmember-fix x)
                                ps)
         (vl-pp-structmember-fn x ps)))

Theorem: vl-pp-dimension-fn-of-vl-dimension-fix-x

(defthm vl-pp-dimension-fn-of-vl-dimension-fix-x
  (equal (vl-pp-dimension-fn (vl-dimension-fix x)
                             ps)
         (vl-pp-dimension-fn x ps)))

Theorem: vl-pp-dimensionlist-fn-of-vl-dimensionlist-fix-x

(defthm vl-pp-dimensionlist-fn-of-vl-dimensionlist-fix-x
  (equal (vl-pp-dimensionlist-fn (vl-dimensionlist-fix x)
                                 ps)
         (vl-pp-dimensionlist-fn x ps)))

Theorem: vl-pp-enumitem-fn-of-vl-enumitem-fix-x

(defthm vl-pp-enumitem-fn-of-vl-enumitem-fix-x
  (equal (vl-pp-enumitem-fn (vl-enumitem-fix x)
                            ps)
         (vl-pp-enumitem-fn x ps)))

Theorem: vl-pp-enumitemlist-fn-of-vl-enumitemlist-fix-x

(defthm vl-pp-enumitemlist-fn-of-vl-enumitemlist-fix-x
  (equal (vl-pp-enumitemlist-fn (vl-enumitemlist-fix x)
                                ps)
         (vl-pp-enumitemlist-fn x ps)))

Theorem: vl-pp-evatom-fn-of-vl-evatom-fix-x

(defthm vl-pp-evatom-fn-of-vl-evatom-fix-x
  (equal (vl-pp-evatom-fn (vl-evatom-fix x) ps)
         (vl-pp-evatom-fn x ps)))

Theorem: vl-pp-evatomlist-fn-of-vl-evatomlist-fix-x

(defthm vl-pp-evatomlist-fn-of-vl-evatomlist-fix-x
  (equal (vl-pp-evatomlist-fn (vl-evatomlist-fix x)
                              ps)
         (vl-pp-evatomlist-fn x ps)))

Theorem: vl-pp-indexlist-fn-vl-exprlist-equiv-congruence-on-x

(defthm vl-pp-indexlist-fn-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-pp-indexlist-fn x ps)
                  (vl-pp-indexlist-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-hidindex-fn-vl-hidindex-equiv-congruence-on-x

(defthm vl-pp-hidindex-fn-vl-hidindex-equiv-congruence-on-x
  (implies (vl-hidindex-equiv x x-equiv)
           (equal (vl-pp-hidindex-fn x ps)
                  (vl-pp-hidindex-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-hidexpr-fn-vl-hidexpr-equiv-congruence-on-x

(defthm vl-pp-hidexpr-fn-vl-hidexpr-equiv-congruence-on-x
  (implies (vl-hidexpr-equiv x x-equiv)
           (equal (vl-pp-hidexpr-fn x ps)
                  (vl-pp-hidexpr-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-scopeexpr-fn-vl-scopeexpr-equiv-congruence-on-x

(defthm vl-pp-scopeexpr-fn-vl-scopeexpr-equiv-congruence-on-x
  (implies (vl-scopeexpr-equiv x x-equiv)
           (equal (vl-pp-scopeexpr-fn x ps)
                  (vl-pp-scopeexpr-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-range-fn-vl-range-equiv-congruence-on-x

(defthm vl-pp-range-fn-vl-range-equiv-congruence-on-x
  (implies (vl-range-equiv x x-equiv)
           (equal (vl-pp-range-fn x ps)
                  (vl-pp-range-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-plusminus-fn-vl-plusminus-equiv-congruence-on-x

(defthm vl-pp-plusminus-fn-vl-plusminus-equiv-congruence-on-x
  (implies (vl-plusminus-equiv x x-equiv)
           (equal (vl-pp-plusminus-fn x ps)
                  (vl-pp-plusminus-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-partselect-fn-vl-partselect-equiv-congruence-on-x

(defthm vl-pp-partselect-fn-vl-partselect-equiv-congruence-on-x
  (implies (vl-partselect-equiv x x-equiv)
           (equal (vl-pp-partselect-fn x ps)
                  (vl-pp-partselect-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-arrayrange-fn-vl-arrayrange-equiv-congruence-on-x

(defthm vl-pp-arrayrange-fn-vl-arrayrange-equiv-congruence-on-x
  (implies (vl-arrayrange-equiv x x-equiv)
           (equal (vl-pp-arrayrange-fn x ps)
                  (vl-pp-arrayrange-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-streamexpr-fn-vl-streamexpr-equiv-congruence-on-x

(defthm vl-pp-streamexpr-fn-vl-streamexpr-equiv-congruence-on-x
  (implies (vl-streamexpr-equiv x x-equiv)
           (equal (vl-pp-streamexpr-fn x ps)
                  (vl-pp-streamexpr-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-streamexprlist-fn-vl-streamexprlist-equiv-congruence-on-x

(defthm
    vl-pp-streamexprlist-fn-vl-streamexprlist-equiv-congruence-on-x
  (implies (vl-streamexprlist-equiv x x-equiv)
           (equal (vl-pp-streamexprlist-fn x ps)
                  (vl-pp-streamexprlist-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-valuerange-fn-vl-valuerange-equiv-congruence-on-x

(defthm vl-pp-valuerange-fn-vl-valuerange-equiv-congruence-on-x
  (implies (vl-valuerange-equiv x x-equiv)
           (equal (vl-pp-valuerange-fn x ps)
                  (vl-pp-valuerange-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-valuerangelist-fn-vl-valuerangelist-equiv-congruence-on-x

(defthm
    vl-pp-valuerangelist-fn-vl-valuerangelist-equiv-congruence-on-x
  (implies (vl-valuerangelist-equiv x x-equiv)
           (equal (vl-pp-valuerangelist-fn x ps)
                  (vl-pp-valuerangelist-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-patternkey-fn-vl-patternkey-equiv-congruence-on-x

(defthm vl-pp-patternkey-fn-vl-patternkey-equiv-congruence-on-x
  (implies (vl-patternkey-equiv x x-equiv)
           (equal (vl-pp-patternkey-fn x ps)
                  (vl-pp-patternkey-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-keyvallist-fn-vl-keyvallist-equiv-congruence-on-x

(defthm vl-pp-keyvallist-fn-vl-keyvallist-equiv-congruence-on-x
  (implies (vl-keyvallist-equiv x x-equiv)
           (equal (vl-pp-keyvallist-fn x ps)
                  (vl-pp-keyvallist-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-assignpat-fn-vl-assignpat-equiv-congruence-on-x

(defthm vl-pp-assignpat-fn-vl-assignpat-equiv-congruence-on-x
  (implies (vl-assignpat-equiv x x-equiv)
           (equal (vl-pp-assignpat-fn x ps)
                  (vl-pp-assignpat-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-casttype-fn-vl-casttype-equiv-congruence-on-x

(defthm vl-pp-casttype-fn-vl-casttype-equiv-congruence-on-x
  (implies (vl-casttype-equiv x x-equiv)
           (equal (vl-pp-casttype-fn x ps)
                  (vl-pp-casttype-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-expr-fn-vl-expr-equiv-congruence-on-x

(defthm vl-pp-expr-fn-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-pp-expr-fn x ps)
                  (vl-pp-expr-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-exprlist-fn-vl-exprlist-equiv-congruence-on-x

(defthm vl-pp-exprlist-fn-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-pp-exprlist-fn x ps)
                  (vl-pp-exprlist-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-maybe-exprlist-fn-vl-maybe-exprlist-equiv-congruence-on-x

(defthm
    vl-pp-maybe-exprlist-fn-vl-maybe-exprlist-equiv-congruence-on-x
  (implies (vl-maybe-exprlist-equiv x x-equiv)
           (equal (vl-pp-maybe-exprlist-fn x ps)
                  (vl-pp-maybe-exprlist-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-call-namedargs-fn-vl-call-namedargs-equiv-congruence-on-x

(defthm
    vl-pp-call-namedargs-fn-vl-call-namedargs-equiv-congruence-on-x
  (implies (vl-call-namedargs-equiv x x-equiv)
           (equal (vl-pp-call-namedargs-fn x ps)
                  (vl-pp-call-namedargs-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-atts-aux-fn-vl-atts-equiv-congruence-on-x

(defthm vl-pp-atts-aux-fn-vl-atts-equiv-congruence-on-x
  (implies (vl-atts-equiv x x-equiv)
           (equal (vl-pp-atts-aux-fn x ps)
                  (vl-pp-atts-aux-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-atts-fn-vl-atts-equiv-congruence-on-x

(defthm vl-pp-atts-fn-vl-atts-equiv-congruence-on-x
  (implies (vl-atts-equiv x x-equiv)
           (equal (vl-pp-atts-fn x ps)
                  (vl-pp-atts-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-datatype-fn-vl-datatype-equiv-congruence-on-x

(defthm vl-pp-datatype-fn-vl-datatype-equiv-congruence-on-x
  (implies (vl-datatype-equiv x x-equiv)
           (equal (vl-pp-datatype-fn x ps)
                  (vl-pp-datatype-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-structmemberlist-fn-vl-structmemberlist-equiv-congruence-on-x

(defthm
 vl-pp-structmemberlist-fn-vl-structmemberlist-equiv-congruence-on-x
 (implies (vl-structmemberlist-equiv x x-equiv)
          (equal (vl-pp-structmemberlist-fn x ps)
                 (vl-pp-structmemberlist-fn x-equiv ps)))
 :rule-classes :congruence)

Theorem: vl-pp-structmember-fn-vl-structmember-equiv-congruence-on-x

(defthm vl-pp-structmember-fn-vl-structmember-equiv-congruence-on-x
  (implies (vl-structmember-equiv x x-equiv)
           (equal (vl-pp-structmember-fn x ps)
                  (vl-pp-structmember-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-dimension-fn-vl-dimension-equiv-congruence-on-x

(defthm vl-pp-dimension-fn-vl-dimension-equiv-congruence-on-x
  (implies (vl-dimension-equiv x x-equiv)
           (equal (vl-pp-dimension-fn x ps)
                  (vl-pp-dimension-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-dimensionlist-fn-vl-dimensionlist-equiv-congruence-on-x

(defthm
      vl-pp-dimensionlist-fn-vl-dimensionlist-equiv-congruence-on-x
  (implies (vl-dimensionlist-equiv x x-equiv)
           (equal (vl-pp-dimensionlist-fn x ps)
                  (vl-pp-dimensionlist-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-enumitem-fn-vl-enumitem-equiv-congruence-on-x

(defthm vl-pp-enumitem-fn-vl-enumitem-equiv-congruence-on-x
  (implies (vl-enumitem-equiv x x-equiv)
           (equal (vl-pp-enumitem-fn x ps)
                  (vl-pp-enumitem-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-enumitemlist-fn-vl-enumitemlist-equiv-congruence-on-x

(defthm vl-pp-enumitemlist-fn-vl-enumitemlist-equiv-congruence-on-x
  (implies (vl-enumitemlist-equiv x x-equiv)
           (equal (vl-pp-enumitemlist-fn x ps)
                  (vl-pp-enumitemlist-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-evatom-fn-vl-evatom-equiv-congruence-on-x

(defthm vl-pp-evatom-fn-vl-evatom-equiv-congruence-on-x
  (implies (vl-evatom-equiv x x-equiv)
           (equal (vl-pp-evatom-fn x ps)
                  (vl-pp-evatom-fn x-equiv ps)))
  :rule-classes :congruence)

Theorem: vl-pp-evatomlist-fn-vl-evatomlist-equiv-congruence-on-x

(defthm vl-pp-evatomlist-fn-vl-evatomlist-equiv-congruence-on-x
  (implies (vl-evatomlist-equiv x x-equiv)
           (equal (vl-pp-evatomlist-fn x ps)
                  (vl-pp-evatomlist-fn x-equiv ps)))
  :rule-classes :congruence)

Subtopics

Vl-pp-valuerangelist
Vl-pp-valuerange
Vl-pp-structmemberlist
Vl-pp-structmember
Vl-pp-streamexprlist
Vl-pp-streamexpr
Vl-pp-scopeexpr
Vl-pp-range
Vl-pp-plusminus
Vl-pp-patternkey
Vl-pp-partselect
Vl-pp-maybe-exprlist
Vl-pp-keyvallist
Vl-pp-indexlist
Vl-pp-hidindex
Vl-pp-hidexpr
Vl-pp-exprlist
Vl-pp-evatomlist
Vl-pp-evatom
Vl-pp-enumitemlist
Vl-pp-enumitem
Vl-pp-dimensionlist
Vl-pp-dimension
Vl-pp-datatype
Vl-pp-casttype
Vl-pp-call-namedargs
Vl-pp-atts-aux
Vl-pp-atts
Vl-pp-assignpat
Vl-pp-arrayrange